- match p1 with [ quintuple x1 y1 z1 w1 v1 ⇒
- match p2 with [ quintuple x2 y2 z2 w2 v2 ⇒
- (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 w1 w2) ⊗ (f5 v1 v2) ]].
+λp1,p2:Prod5T T1 T2 T3 T4 T5.
+ (f1 (fst5T … p1) (fst5T … p2)) ⊗
+ (f2 (snd5T … p1) (snd5T … p2)) ⊗
+ (f3 (thd5T … p1) (thd5T … p2)) ⊗
+ (f4 (fth5T … p1) (fth5T … p2)) ⊗
+ (f5 (fft5T … p1) (fft5T … p2)).