...

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / relations_to_o-algebra.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
index 7f2710640ddf83d38385b9b15380644ac33ee8bc..2368affe0fca9711d74ff0395518b28483f10a4b 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
@@ -168,9 +168,7 @@ definition SUBSETS': carr3 (arrows3 CAT2 (category2_of_category1 REL) OA).
      [ apply (orelation_of_relation S T);
      | intros; apply (orelation_of_relation_preserves_equality S T a a' e); ]
   | apply orelation_of_relation_preserves_identity;
-  | simplify; intros;
-    apply (.= (orelation_of_relation_preserves_composition o1 o2 o4 f1 (f3∘f2)));
-    apply (#‡(orelation_of_relation_preserves_composition o2 o3 o4 f2 f3)); ]
+  | apply orelation_of_relation_preserves_composition; ]
 qed.
 
 theorem SUBSETS_faithful: