Function prop::fun::tup3_eq_snd

pub fn tup3_eq_snd<A: Prop, B: Prop, C: Prop, D: Prop>(
    x: Eq<A, B>
) -> Eq<Tup3<C, A, D>, Tup3<C, B, D>>

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