const In : set set prop term iIn = In infix iIn 2000 2000 term PNoEq_ = \x:set.\p:set prop.\q:set prop.!y:set.y iIn x -> (p y <-> q y) axiom iff_refl: !P:prop.P <-> P claim !x:set.!p:set prop.!y:set.y iIn x -> (p y <-> p y)