pub fn exc_both<A: Prop, B: Prop>( ((not_a, not_b), x): And<And<Not<A>, Not<B>>, Or<A, B>>) -> False
(¬a ∧ ¬b) ∧ (a ∨ b) => a
