some notation for map_arrows2

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

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 b24a730cb05381873fc80103b8491ab1288e6f8e..5cb82832a167a8bafa07910d59b8c5e60e973a93 100644 (file)
--- 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 ?????));