Theory "normalForms"

Parents     bool

Signature

Constant Type
UNIV_POINT :('a -> bool) -> 'a
EXT_POINT :('a -> 'b) -> ('a -> 'b) -> 'a

Definitions

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

Theorems

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