Function prop::imply::rev_modus_tollens_eq_excm

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

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