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
⊢ ∀f g. f (EXT_POINT f g) = g (EXT_POINT f g) ⇔ f = g
⊢ ∀p. p (UNIV_POINT p) ⇔ ∀x. p x