Theory "normalForms"

Parents bool

Signature

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

EXT_POINT_DEF

⊢ ∀f g. f (EXT_POINT f g) = g (EXT_POINT f g) ⇒ f = g

UNIV_POINT_DEF

⊢ ∀p. p (UNIV_POINT p) ⇒ ∀x. p x

EXT_POINT

⊢ ∀f g. f (EXT_POINT f g) = g (EXT_POINT f g) ⇔ f = g

UNIV_POINT

⊢ ∀p. p (UNIV_POINT p) ⇔ ∀x. p x