added a simplify to prevent the generation of an ugly fix

[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..36bea989eede832c212ec7b41abb078f3e6db1a4 100644 (file)
--- 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