Dummy dependent products in inductive types arities are no longer cleaned.

[helm.git] / helm / software / matita / library / technicalities / setoids.ma

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index f9c5e878bf1490346d82810827c2aea0d9470f36..4c51d3a448e15a900e8b28f2118cb480139614fd 100644 (file)
--- a/helm/software/matita/library/technicalities/setoids.ma
+++ b/helm/software/matita/library/technicalities/setoids.ma
@@ -694,9 +694,10 @@ theorem apply_morphism_compatibility_Right2Left:
      generalize in match H2; clear H2;
      elim args2 0; clear args2;
      elim args1; clear args1;
+     simplify in H2;
+     change in H2:(? ? %) with 
+       (relation_of_product_of_arguments Right2Left n t2 t4);
      elim H2; clear H2;
-     change in H4 with
-      (relation_of_product_of_arguments Right2Left n t2 t4);
      change with
       (relation_of_relation_class unit Out (apply_morphism n Out (m1 t3) t4)
         (apply_morphism n Out (m2 t1) t2));
@@ -816,9 +817,9 @@ theorem apply_morphism_compatibility_Left2Right:
      generalize in match H2; clear H2;
      elim args2 0; clear args2;
      elim args1; clear args1;
+     simplify in H2; change in H2:(? ? %) with
+       (relation_of_product_of_arguments Left2Right n t2 t4); 
      elim H2; clear H2;
-     change in H4 with
-      (relation_of_product_of_arguments Left2Right n t2 t4);
      change with
       (relation_of_relation_class unit Out (apply_morphism n Out (m1 t1) t2)
         (apply_morphism n Out (m2 t3) t4));
@@ -898,7 +899,7 @@ definition interp :
      rewrite <
        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
      exact c1
-   | split;
+   | simplify;split;
       [ rewrite <
          (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
         exact c1
@@ -929,7 +930,7 @@ definition interp_relation_class_list :
      rewrite <
        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
      exact c1
-  | split;
+  | simplify; split;
      [ rewrite <
         (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
        exact c1