Function prop::eq::contra

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

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