some notation added with a bit PITA

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

diff --git a/helm/software/matita/contribs/dama/dama/models/uniformnat.ma b/helm/software/matita/contribs/dama/dama/models/uniformnat.ma
index 8c0acd9a2f1a0d54fb352936eb2690610a76bec5..824d6c29319ebec9a742a863316b28f2247e170e 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/uniformnat.ma
+++ b/helm/software/matita/contribs/dama/dama/models/uniformnat.ma
@@ -19,14 +19,14 @@ include "uniform.ma".
 definition discrete_uniform_space_of_bishop_set:bishop_set → uniform_space.
 intro C; apply (mk_uniform_space C);
 [1: intro; apply (∃_:unit.∀n:C square.(fst n ≈ snd n → P n) ∧ (P n → fst n ≈ snd n)); 
-|2: intros 4 (U H x Hx); unfold in Hx;
+|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); 
     exists[apply (λx.U x ∧ V x)] split;
     [1: exists[apply something] intro; cases (PU n); cases (PV n);
         split; intros; try split;[apply H2;|apply H4] try assumption;
         apply H3; cases H6; assumption;
-    |2: simplify; unfold mk_set; intros; assumption;]
+    |2: simplify; intros; assumption;]
 |4: intros; cases H (_ PU); exists [apply U] split;
     [1: exists [apply something] intro n; cases (PU n);
         split; intros; try split;[apply H1;|apply H2] assumption;
@@ -95,13 +95,12 @@ split;
     cases Hcut1; assumption]
 qed.
 
-alias symbol "pi1" = "sigma pi1".
+alias symbol "pi1" = "exT fst".
 lemma nat_dedekind_sigma_complete:
   ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing → 
     ∀x.x is_supremum a → ∃i.∀j.i ≤ j → fst x = fst (a j).
-intros 5; cases x (s Hs); clear x; letin X ≝ (sig_in ℕ (λx:ℕ.x∈[l,u]) s Hs); 
+intros 5; cases x (s Hs); clear x; letin X ≝ (〈s,Hs〉); 
 fold normalize X; intros; cases H1; 
-alias symbol "pi1" = "sigma pi1".
 letin spec ≝ (λi,j.fst (a j) = s ∨ (i ≤ j ∧ match i with [ O ⇒ fst (a j) = fst (a O) | S m ⇒ fst(a m) < fst (a j)]));
 letin m ≝ (
   let rec aux i ≝
@@ -144,7 +143,7 @@ letin m ≝ (
             apply os_le_to_nat_le; lapply (nat_le_to_os_le ?? H7) as H77;
             apply(trans_increasing ?? H (S n2) (pred) H77);]]]]] 
 clearbody m; unfold spec in m; clear spec;
-cut (∀i.fst a (m i) = s ∨ i ≤ fst (a (m i))) as key2;[ 
+cut (∀i.fst (a (m i)) = s ∨ i ≤ fst (a (m i))) as key2;[ 
 letin find ≝ (
  let rec find i u on u : nat ≝
   match u with