X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcommon%2Fprod.ma;h=1080533d174f6ea77cecf45b84be841f6d193c6b;hb=73052ec76ff5492989f9cbae2ebe0b770fcb985f;hp=fca58bc223094c7cf2220813a95d182fb4c6fa35;hpb=5683cf231fa2ac8abade3b70aea1af995cc04379;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/common/prod.ma b/helm/software/matita/contribs/ng_assembly/common/prod.ma
index fca58bc22..1080533d1 100644
--- a/helm/software/matita/contribs/ng_assembly/common/prod.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/prod.ma
@@ -36,8 +36,9 @@ ndefinition snd ≝
 λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair  _ x ⇒ x ].
 
 ndefinition eq_pair ≝
-λT1,T2:Type.λp1,p2:ProdT T1 T2.
+λT1,T2:Type.
 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.
+λp1,p2:ProdT T1 T2.
  (f1 (fst … p1) (fst … p2)) ⊗
  (f2 (snd … p1) (snd … p2)).
 
@@ -54,8 +55,9 @@ ndefinition thd3T ≝
 λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple _ _ x ⇒ x ].
 
 ndefinition eq_triple ≝
-λT1,T2,T3:Type.λp1,p2:Prod3T T1 T2 T3.
+λT1,T2,T3:Type.
 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.
+λp1,p2:Prod3T T1 T2 T3.
  (f1 (fst3T … p1) (fst3T … p2)) ⊗
  (f2 (snd3T … p1) (snd3T … p2)) ⊗
  (f3 (thd3T … p1) (thd3T … p2)).
@@ -76,8 +78,9 @@ ndefinition fth4T ≝
 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ _ _ x ⇒ x ].
 
 ndefinition eq_quadruple ≝
-λT1,T2,T3,T4:Type.λp1,p2:Prod4T T1 T2 T3 T4.
+λT1,T2,T3,T4:Type.
 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.
+λp1,p2:Prod4T T1 T2 T3 T4.
  (f1 (fst4T … p1) (fst4T … p2)) ⊗
  (f2 (snd4T … p1) (snd4T … p2)) ⊗
  (f3 (thd4T … p1) (thd4T … p2)) ⊗
@@ -102,8 +105,9 @@ ndefinition fft5T ≝
 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ _ x ⇒ x ].
 
 ndefinition eq_quintuple ≝
-λT1,T2,T3,T4,T5:Type.λp1,p2:Prod5T T1 T2 T3 T4 T5.
+λT1,T2,T3,T4,T5:Type.
 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.λf5:T5 → T5 → bool.
+λp1,p2:Prod5T T1 T2 T3 T4 T5.
  (f1 (fst5T … p1) (fst5T … p2)) ⊗
  (f2 (snd5T … p1) (snd5T … p2)) ⊗
  (f3 (thd5T … p1) (thd5T … p2)) ⊗