Function prop::fun::tup_eq_fst

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

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