Function prop::and::eq_left

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

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