Function prop::eq::rev_modus_tollens_eq_excm

pub fn rev_modus_tollens_eq_excm<A: Prop, B: Prop>(
    (f0, f1): Eq<Not<A>, Not<B>>,
    eq_excm_a_excm_b: Eq<ExcM<A>, ExcM<B>>
) -> Eq<B, A>

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