Function prop::eq::neq_left

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).