Function prop::and::eq_right

pub fn eq_right<A: Prop, B: Prop, C: Prop>(
    (ab, ba): Eq<A, B>
) -> Eq<And<C, A>, And<C, B>>

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