some added lemmas removed from auto

[helm.git] / helm / software / matita / nlibrary / topology / cantor.ma

diff --git a/helm/software/matita/nlibrary/topology/cantor.ma b/helm/software/matita/nlibrary/topology/cantor.ma
index d3dccb8ee07e66248e17e69f21536cc6fb3013fe..6a79dd2d808df2478f6a4ad25568e41e1eb68894 100644 (file)
--- a/helm/software/matita/nlibrary/topology/cantor.ma
+++ b/helm/software/matita/nlibrary/topology/cantor.ma
@@ -78,7 +78,7 @@ alias id "S" = "cic:/matita/ng/topology/igft/S.fix(0,0,1)".
 unification hint 0 ≔ ;
          x ≟ axs  
   (* -------------- *) ⊢
-         S x ≡ A. 
+         S (uax x) ≡ A. (* XXX: bug coercions/ disamb multipasso che ne fa 1 solo*) 
 
 ntheorem col2_4 :
   ∀A:uAx.∀a:uax A. a ◃ ∅ → ¬ a ∈ 𝐂 a one.
@@ -88,7 +88,8 @@ ntheorem col2_4 :
 ##]
 nqed.
 
-ndefinition Z : Ω^axs ≝ { x | x ◃ ∅ }.
+(* bug interpretazione non aggiunta per ∅ *)
+ndefinition Z : Ω^axs ≝ { x | x ◃ (emptyset ?) }.
 
 ntheorem cover_monotone: ∀A:Ax.∀a:A.∀U,V.U ⊆ V → a ◃ U → a ◃ V.
 #A; #a; #U; #V; #HUV; #H; nelim H; /3/; 
@@ -126,7 +127,7 @@ alias id "S" = "cic:/matita/ng/topology/igft/S.fix(0,0,1)".
 unification hint 0 ≔ ;
          x ≟ caxs  
   (* -------------- *) ⊢
-         S x ≡ nat. 
+         S (uax x) ≡ nat. 
 
 naxiom h : nat → nat.