axiom xm: !P:prop.P | ~ P axiom prop_ext_2: !P:prop.!Q:prop.(P -> Q) -> (Q -> P) -> P = Q axiom func_ext: !P:prop prop.!Q:prop prop.(!R:prop.P R = Q R) -> P = Q claim or = \P:prop.\Q:prop.~ (~ P & ~ Q)