Function prop::and::rev_eq_left_true

pub fn rev_eq_left_true<A: Prop, B: Prop, C: Prop>(
    (f, g): Eq<And<A, C>, And<B, C>>,
    c: C
) -> Eq<A, B>

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