X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ftechnicalities%2Fsetoids.ma;fp=helm%2Fsoftware%2Fmatita%2Flibrary%2Ftechnicalities%2Fsetoids.ma;h=36bea989eede832c212ec7b41abb078f3e6db1a4;hb=60218a0347847f6797575c7fa33a98ac6862e6cf;hp=f9c5e878bf1490346d82810827c2aea0d9470f36;hpb=34b3404a33922e9c4b8f25c7b14dadd260990de3;p=helm.git

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index f9c5e878b..36bea989e 100644
--- a/helm/software/matita/library/technicalities/setoids.ma
+++ b/helm/software/matita/library/technicalities/setoids.ma
@@ -929,7 +929,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