Function prop::fun::tup3_rev_eq_trd

pub fn tup3_rev_eq_trd<A: Prop, B: Prop, C: Prop, D: Prop, X: Prop, Y: Prop>(
    ty_c: Ty<C, X>,
    ty_d: Ty<D, Y>,
    x: Eq<Tup3<C, D, A>, Tup3<C, D, B>>
) -> Eq<A, B>

(c : x) ⋀ (d : y) ⋀ ((c, d, a) == (c, d, b)) => (a == b).