Using Prop conjuction on Props lowers the universes.

[helm.git] / helm / software / matita / contribs / dama / dama / models / discrete_uniformity.ma

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 412b5407dd0e6816c7b7c5d78f9e41725898c61b..01890a416346c9afa546d5c9d7020fa4569f1234 100644 (file)
--- 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 square.(\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);