Function prop::eq::rev_modus_tollens_imply_excm

pub fn rev_modus_tollens_imply_excm<A: Prop, B: Prop>(
    (f0, f1): Eq<Not<A>, Not<B>>,
    a_excm_b: Imply<A, ExcM<B>>,
    b_excm_a: Imply<B, ExcM<A>>
) -> Eq<B, A>

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