shifting done, merge attacked

[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 8063ea0bfcf43bc38b566562e4a577bff973c254..412b5407dd0e6816c7b7c5d78f9e41725898c61b 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 (∃_: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); 
@@ -34,8 +34,8 @@ intro C; apply (mk_uniform_space C);
     [1: exists [apply something] intro n; cases (PU n);
         split; intros; try split;[apply H1;|apply H2] assumption;
     |2: intros 2 (x Hx); cases Hx; cases H1; clear H1;
-        cases (PU 〈(fst x),x1〉); lapply (H4 H2) as H5; simplify in H5;
-        cases (PU 〈x1,(snd x)〉); lapply (H7 H3) as H8; simplify in H8;
+        cases (PU 〈(\fst x),x1〉); lapply (H4 H2) as H5; simplify in H5;
+        cases (PU 〈x1,(\snd x)〉); lapply (H7 H3) as H8; simplify in H8;
         generalize in match H5; generalize in match H8;
         generalize in match (PU x); clear H6 H7 H1 H4 H2 H3 H5 H8; 
         cases x; simplify; intros; cases H1; clear H1; apply H4;