X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ftechnicalities%2Fsetoids.ma;h=4c51d3a448e15a900e8b28f2118cb480139614fd;hb=347b0f483245bd0295f95f99742e23484c331312;hp=78b58ba314ddb8f0ac76613cfe3f95bee55af42e;hpb=ce3c2e0c887e0f8303ae9c15e22bc7e29bb89462;p=helm.git

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index 78b58ba31..4c51d3a44 100644
--- a/helm/software/matita/library/technicalities/setoids.ma
+++ b/helm/software/matita/library/technicalities/setoids.ma
@@ -817,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));