axiom FalseE: ~ False axiom xm: !P:prop.P | ~ P claim !P:prop.~ ~ P -> P