X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fmodels%2Fdiscrete_uniformity.ma;h=76461f3f46222f911f4a366a90d8360cfd9ca426;hb=7deb4b1f322850b8ff03d5626f7828736d074ec8;hp=01890a416346c9afa546d5c9d7020fa4569f1234;hpb=342f51f2886fbb01457db47b313b5120dd002531;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma b/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma
index 01890a416..76461f3f4 100644
--- a/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma
+++ b/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma
@@ -21,7 +21,7 @@ intro C; apply (mk_uniform_space C);
     alias symbol "pi2" = "pair pi2".
     alias symbol "pi1" = "pair pi1".
     alias symbol "and" = "logical and".
-    apply (∃d:unit.∀n:C square.(\fst n ≈ \snd n → P n) ∧ (P n → \fst n ≈ \snd n)); 
+    apply (∃d:unit.∀n:C squareB.(\fst n ≈ \snd n → P n) ∧ (P n → \fst n ≈ \snd n)); 
 |2: intros 4 (U H x Hx); simplify in Hx;
     cases H (_ H1); cases (H1 x); apply H2; apply Hx;
 |3: intros; cases H (_ PU); cases H1 (_ PV);