-ndefinition Prod5T_ind
- : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Prop.
- (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
- Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
-λT1,T2,T3,T4,T5:Type.λP:Prod5T T1 T2 T3 T4 T5 → Prop.
-λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4).
-λp:Prod5T T1 T2 T3 T4 T5.
- match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
-
-ndefinition Prod5T_rec
- : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Set.
- (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
- Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
-λT1,T2,T3,T4,T5:Type.λP:Prod5T T1 T2 T3 T4 T5 → Set.
-λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4).
-λp:Prod5T T1 T2 T3 T4 T5.
- match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
-
-ndefinition Prod5T_rect
- : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Type.
- (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
- Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
-λT1,T2,T3,T4,T5:Type.λP:Prod5T T1 T2 T3 T4 T5 → Type.
-λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4).
-λp:Prod5T T1 T2 T3 T4 T5.
- match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
-