Function prop::and::to_eq_neg

pub fn to_eq_neg<A: Prop, B: Prop>((f0, f1): And<Not<A>, Not<B>>) -> Eq<A, B>

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