Function prop::fun::par_tup_fun_ty

pub fn par_tup_fun_ty<F: Prop, G: Prop, X1: Prop, X2: Prop, Y1: Prop, Y2: Prop>(
    _ty_f: Ty<F, Pow<Y1, X1>>,
    _ty_g: Ty<G, Pow<Y2, X2>>
) -> Ty<App<ParTup, Tup<F, G>>, Pow<Tup<Y1, Y2>, Tup<X1, X2>>>

(f : (x1 -> y1)) ⋀ (g : (x2 -> y2)) => (f x g) : ((x1, x2) -> (y1, y2)).