X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly2%2Fcommon%2Fprod.ma;h=5de6fb42ebe983041803fbb4fad90d7fc2e14fb3;hb=HEAD;hp=38852d1a9b2be36f9d3bb5580ad3c5e2e5bd3239;hpb=bd112857523fc543c78cd29b74417585033ec464;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly2/common/prod.ma b/helm/software/matita/contribs/ng_assembly2/common/prod.ma
index 38852d1a9..5de6fb42e 100644
--- a/helm/software/matita/contribs/ng_assembly2/common/prod.ma
+++ b/helm/software/matita/contribs/ng_assembly2/common/prod.ma
@@ -186,7 +186,9 @@ nlemma pair_is_comparable :
  comparable → comparable → comparable.
  #T1; #T2; napply (mk_comparable (ProdT T1 T2));
  ##[ napply (pair … (zeroc T1) (zeroc T2))
- ##| napply (λx.false)
+ ##| napply (λP.(forallc T1)
+             (λe1.(forallc T2)
+              (λe2.P (pair … e1 e2))))
  ##| napply (eq_pair … (eqc T1) (eqc T2))
  ##| napply (eqpair_to_eq … (eqc T1) (eqc T2));
      ##[ napply (eqc_to_eq T1)
@@ -428,7 +430,10 @@ nlemma triple_is_comparable :
  comparable → comparable → comparable → comparable.
  #T1; #T2; #T3; napply (mk_comparable (Prod3T T1 T2 T3));
  ##[ napply (triple … (zeroc T1) (zeroc T2) (zeroc T3))
- ##| napply (λx.false)
+ ##| napply (λP.(forallc T1)
+             (λe1.(forallc T2)
+              (λe2.(forallc T3)
+               (λe3.P (triple … e1 e2 e3)))))
  ##| napply (eq_triple … (eqc T1) (eqc T2) (eqc T3))
  ##| napply (eqtriple_to_eq … (eqc T1) (eqc T2) (eqc T3));
      ##[ napply (eqc_to_eq T1)
@@ -719,7 +724,11 @@ nlemma quadruple_is_comparable :
  comparable → comparable → comparable → comparable → comparable.
  #T1; #T2; #T3; #T4; napply (mk_comparable (Prod4T T1 T2 T3 T4));
  ##[ napply (quadruple … (zeroc T1) (zeroc T2) (zeroc T3) (zeroc T4))
- ##| napply (λx.false)
+ ##| napply (λP.(forallc T1)
+             (λe1.(forallc T2)
+              (λe2.(forallc T3)
+               (λe3.(forallc T4)
+                (λe4.P (quadruple … e1 e2 e3 e4))))))
  ##| napply (eq_quadruple … (eqc T1) (eqc T2) (eqc T3) (eqc T4))
  ##| napply (eqquadruple_to_eq … (eqc T1) (eqc T2) (eqc T3) (eqc T4));
      ##[ napply (eqc_to_eq T1)
@@ -1059,7 +1068,12 @@ nlemma quintuple_is_comparable :
  comparable → comparable → comparable → comparable → comparable → comparable.
  #T1; #T2; #T3; #T4; #T5; napply (mk_comparable (Prod5T T1 T2 T3 T4 T5));
  ##[ napply (quintuple … (zeroc T1) (zeroc T2) (zeroc T3) (zeroc T4) (zeroc T5))
- ##| napply (λx.false)
+ ##| napply (λP.(forallc T1)
+             (λe1.(forallc T2)
+              (λe2.(forallc T3)
+               (λe3.(forallc T4)
+                (λe4.(forallc T5)
+                 (λe5.P (quintuple … e1 e2 e3 e4 e5)))))))
  ##| napply (eq_quintuple … (eqc T1) (eqc T2) (eqc T3) (eqc T4) (eqc T5))
  ##| napply (eqquintuple_to_eq … (eqc T1) (eqc T2) (eqc T3) (eqc T4) (eqc T5));
      ##[ napply (eqc_to_eq T1)