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=e2a6d130d5274760f4591197bbbc66c3191e8a6a;hp=412b5407dd0e6816c7b7c5d78f9e41725898c61b;hpb=ca41435a6021292ccba239aa173651c0be705b45;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 412b5407d..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 (∃_: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);