pub fn eqq_to_excm_q_with_excm_eq<A: Prop, B: Prop>(
    eqq: EqQ<A, B>,
    excm_eq: ExcM<Eq<A, B>>
) -> ExcM<Q<A, B>>
Expand description

eqq(a, b) ⋀ ((a == b) ⋁ ¬(a == b)) => ((a ~~ b) ⋁ ¬(a ~~ b)).