X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fbasic_topologies.ma;h=5cb82832a167a8bafa07910d59b8c5e60e973a93;hb=05cfeb82d2624860e66941421a937f308d66cf33;hp=b24a730cb05381873fc80103b8491ab1288e6f8e;hpb=82b1a205fdf9bc2c8029296ebe94c5667798845b;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma
index b24a730cb..5cb82832a 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma
@@ -145,9 +145,9 @@ definition BTop: category1.
             = minus_star_image o2 o3 b' (A o2 (minus_star_image o1 o2 a' (A o1 X))));
         [2: intro; apply sym1; apply (.= #‡(†((H' ?)\sup -1))); apply sym1; apply (K X);]
        clear K H' H1';
-       alias symbol "compose" (instance 2) = "category1 composition".
-cut (∀X:Ω \sup o1.
-              minus_star_image o1 o3 (b ∘ a) (A o1 X) = minus_star_image o1 o3 (b'∘a') (A o1 X));
+alias symbol "compose" (instance 1) = "category1 composition".
+cut (∀X:Ω^o1.
+              minus_star_image ?? (b ∘ a) (A o1 X) =_1 minus_star_image ?? (b'∘a') (A o1 X));
         [2: intro;
             apply (.= (minus_star_image_comp ??????));
             apply (.= #‡(saturated ?????));