Theory "one"

Signature

Definitions

one_DEF

⊢ () = @x. T

one_TY_DEF

⊢ ∃rep. TYPE_DEFINITION (λb. b) rep

one_case_def

⊢ ∀u x. one_CASE u x = x

Theorems

FORALL_ONE

⊢ (∀x. P x) ⇔ P ()

one

⊢ ∀v. v = ()

one_Axiom

⊢ ∀e. ∃!fn. fn () = e

one_axiom

⊢ ∀f g. f = g

one_case_thm

⊢ ∀x. one_CASE () x = x

one_induction

⊢ ∀P. P () ⇒ ∀x. P x

one_prim_rec

⊢ ∀e. ∃fn. fn () = e