const PNoEq_ : set (set prop) (set prop) prop axiom PNoEq_ref_: !x:set.!p:set prop.PNoEq_ x p p const PNoLe : set (set prop) set (set prop) prop axiom PNoLeI2: !x:set.!p:set prop.!q:set prop.PNoEq_ x p q -> PNoLe x p x q claim !x:set.!p:set prop.PNoLe x p x p