Theory "one"

Parents     sat   combin

Signature

Type Arity
one 0
Constant Type
one :unit
one_CASE :unit -> α -> α

Definitions

one_TY_DEF 
|- ∃rep. TYPE_DEFINITION (λb. b) rep
one_DEF 
|- () = @x. T
one_case_def 
|- ∀u x. (case u of () => x) = x

Theorems

one_axiom 
|- ∀f g. f = g
one 
|- ∀v. v = ()
one_Axiom 
|- ∀e. ∃!fn. fn () = e
one_prim_rec 
|- ∀e. ∃fn. fn () = e
one_induction 
|- ∀P. P () ⇒ ∀x. P x
FORALL_ONE 
|- (∀x. P x) ⇔ P ()
one_case_thm 
|- ∀x. (case () of () => x) = x