all pullbacks are attempted in sequence, removed many unfold

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / o-basic_topologies.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
index 8847eef3157fbdf9c8ec2969894997ea49b4b493..30a8b476cb2045f1ea204e4489dc34c1e54cc2e5 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
@@ -106,10 +106,8 @@ definition continuous_relation_comp:
   | intros;
     apply sym1; 
     change in match ((s ∘ r) U) with (s (r U));
-    (*<BAD>*) unfold FunClass_1_OF_carr2;
-              apply (.= (reduced : ?)\sup -1);
-     [ (*BAD*) change with (eq1 ? (r U) (J ? (r U)));
-       (* BAD U *) apply (.= (reduced ??? U ?)); [ assumption | apply refl1 ]
+    apply (.= (reduced : ?)\sup -1);
+     [ apply (.= (reduced :?)); [ assumption | apply refl1 ]
      | apply refl1]
   | intros;
     apply sym1;