pub fn rev_modus_ponens<A: Prop, B: Prop>(g: Imply<B, A>, f: Not<A>) -> Not<B>
Expand description

(b => a) ∧ ¬a => ¬b.