bool_cases_axiom
b
(b 
T) 
(b F)
_antisym_axiom
b1 b2 (b1 b2) (b2 b1) (b1 b2)
η_axiom
f (
x f x) = f
_axiom
P x P x P ($ P)
infinity_axiom
f OneOne f 
Onto f
