pub fn rev_modus_tollens<A: DProp, B: DProp>( (f0, f1): Eq<Not<A>, Not<B>> ) -> Eq<B, A>
(¬a == ¬b) => (b == a).
(¬a == ¬b) => (b == a)