Function prop::eq::neq_right

pub fn neq_right<A: Prop, B: Prop, C: Prop>(
    eq_ab: Eq<A, B>,
    neq_bc: Not<Eq<B, C>>
) -> Not<Eq<A, C>>

(a == b) ⋀ ¬(b == c) => ¬(a == c).