pub fn bound_neg<A: Prop, B: Prop>(f: Or<And<Not<A>, B>, A>) -> Or<B, A>
(¬a ∧ b) ∨ a => (b ∨ a).
(¬a ∧ b) ∨ a => (b ∨ a)
