pub fn modus_tollens<A: Prop, B: Prop>(f: Imply<A, B>) -> Imply<Not<B>, Not<A>>
a => b => ¬b => ¬a.
a => b => ¬b => ¬a
Swap sides of implication by taking their negation.