Function prop::eq::contra

source · [−]
pub fn contra<A: DProp, B: DProp>(f: Not<Eq<A, B>>, a: A) -> Not<B>
Expand description

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