pub fn neq_left<A: Prop, B: Prop, C: Prop>( eq_ab: Eq<A, B>, neq_ac: Not<Eq<A, C>> ) -> Not<Eq<B, C>>
(a == b) ⋀ ¬(a == c) => ¬(b == c).
(a == b) ⋀ ¬(a == c) => ¬(b == c)