axiom exactly1of2_E: !P:prop.!Q:prop.~(P <-> Q) -> !R:prop.(P -> ~ Q -> R) -> (~ P -> Q -> R) -> R claim !P:prop.!Q:prop.~(P <-> Q) -> P | Q