pub fn to_imply<A: DProp, B: DProp>(f: And<A, Not<B>>) -> Not<Imply<A, B>>
(a ∧ ¬b) => ¬(a => b).
(a ∧ ¬b) => ¬(a => b)
