Function prop::imply::rev_double_neg_imply_excm

pub fn rev_double_neg_imply_excm<A: Prop, B: Prop>(
    f: Imply<Not<Not<A>>, Not<Not<B>>>,
    a_excm_b: Imply<A, ExcM<B>>
) -> Imply<A, B>

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