Theory "normalForms"

Parents     bool

Signature

Constant Type
EXT_POINT :(α -> β) -> (α -> β) -> α
UNIV_POINT :(α -> bool) -> α

Definitions

UNIV_POINT_DEF 
⊢ ∀p. p (UNIV_POINT p) ⇒ ∀x. p x
EXT_POINT_DEF 
⊢ ∀f g. (f (EXT_POINT f g) = g (EXT_POINT f g)) ⇒ (f = g)

Theorems

UNIV_POINT 
⊢ ∀p. p (UNIV_POINT p) ⇔ ∀x. p x
EXT_POINT 
⊢ ∀f g. (f (EXT_POINT f g) = g (EXT_POINT f g)) ⇔ (f = g)