X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Fcantor.ma;h=6ae8d36ad299078b76670460b6b3a0a16016faf3;hb=68bcb81d3d91255eacd5ae4c19c755d41e8440cf;hp=b8f8a5543ad57e8cf24ea8ee2f169e63ac94c0aa;hpb=ab72456f3d53035e6942f1cafa225d6759acf655;p=helm.git

diff --git a/helm/software/matita/nlibrary/topology/cantor.ma b/helm/software/matita/nlibrary/topology/cantor.ma
index b8f8a5543..6ae8d36ad 100644
--- a/helm/software/matita/nlibrary/topology/cantor.ma
+++ b/helm/software/matita/nlibrary/topology/cantor.ma
@@ -28,6 +28,7 @@ interpretation "empty" 'empty = (emptyset ?).
 
 naxiom EM : ∀A:Ax.∀a:A.∀i_star.(a ∈ 𝐂 a i_star) ∨ ¬( a ∈ 𝐂 a i_star).
 
+alias symbol "covers" = "covers".
 ntheorem th2_3 :
   ∀A:Ax.∀a:A. a ◃ ∅ → ∃i. ¬ a ∈ 𝐂 a i.
 #A; #a; #H; nelim H;
@@ -130,6 +131,7 @@ naxiom h : nat → nat.
 alias symbol "eq" = "leibnitz's equality".
 alias symbol "eq" = "setoid1 eq".
 alias symbol "covers" = "covers".
+alias symbol "eq" = "leibnitz's equality".
 naxiom Ph :  ∀x.h x = O \liff  x ◃ ∅.
 
 nlemma replace_char: