Function prop::eq::contra_excm

pub fn contra_excm<A: Prop, B: Prop>(
    f: Not<Eq<A, B>>,
    a: A,
    excm_b: ExcM<B>
) -> Not<B>

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