Theory one

Parents

combin
sat

Contents

Type operators

one : unit

Constants

one : unit
one_CASE : unit -> α -> α

Definitions

one_DEF one_TY_DEF one_case_def

Theorems

EXISTS_ONE_FN FORALL_ONE FORALL_ONE_FN one one_Axiom one_axiom one_case_thm one_induction one_prim_rec

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

EXISTS_ONE_FN

⊢ (∃f. P f) ⇔ ∃f. P (λx u. f x)

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

FORALL_ONE_FN

⊢ (∀uf. P uf) ⇔ ∀a. P (λu. a)

⊢ ∀v. v = ()

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

⊢ ∀f g. f = g

⊢ ∀x. one_CASE () x = x

one_induction

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

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