From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 13 Jun 2008 07:14:52 +0000 (+0000)
Subject: more notation
X-Git-Tag: make_still_working~5032
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3c1ca5620048ad842144fba291f8bc5f0dca7061;p=helm.git

more notation
---

diff --git a/helm/software/matita/contribs/dama/dama/bishop_set.ma b/helm/software/matita/contribs/dama/dama/bishop_set.ma
index d57282079..78176d776 100644
--- a/helm/software/matita/contribs/dama/dama/bishop_set.ma
+++ b/helm/software/matita/contribs/dama/dama/bishop_set.ma
@@ -41,7 +41,7 @@ qed.
 (* Definition 2.2 (2) *)
 definition eq ≝ λA:bishop_set.λa,b:A. ¬ (a # b).
 
-notation "hvbox(a break ≈ b)" non associative with precedence 45 
+notation "hvbox(a break \approx b)" non associative with precedence 45 
   for @{ 'napart $a $b}.
       
 interpretation "Bishop set alikeness" 'napart a b = (eq _ a b). 
@@ -57,7 +57,6 @@ qed.
 lemma eq_sym:∀E:bishop_set.∀x,y:E.x ≈ y → y ≈ x ≝ eq_sym_.
 
 lemma eq_trans_: ∀E:bishop_set.transitive ? (eq E).
-(* bug. intros k deve fare whd quanto basta *)
 intros 6 (E x y z Exy Eyz); intro Axy; cases (bs_cotransitive ???y Axy); 
 [apply Exy|apply Eyz] assumption.
 qed.
diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
index 21c10a4e1..b42eaf61b 100644
--- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
+++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
@@ -15,7 +15,7 @@
 include "logic/equality.ma".
 
 inductive Or (A,B:CProp) : CProp ≝
-   Left : A → Or A B
+ | Left : A → Or A B
  | Right : B → Or A B.
 
 interpretation "constructive or" 'or x y = (Or x y).
@@ -28,14 +28,14 @@ interpretation "constructive and" 'and x y = (And x y).
 inductive And3 (A,B,C:CProp) : CProp ≝
  | Conj3 : A → B → C → And3 A B C.
 
-notation < "a ∧ b ∧ c" left associative with precedence 60 for @{'and3 $a $b $c}.
+notation < "a ∧ b ∧ c" left associative with precedence 35 for @{'and3 $a $b $c}.
  
 interpretation "constructive ternary and" 'and3 x y z = (Conj3 x y z).
 
-inductive And4 (A,B,C:CProp) : CProp ≝
- | Conj4 : A → B → C → And4 A B C.
+inductive And4 (A,B,C,D:CProp) : CProp ≝
+ | Conj4 : A → B → C → D → And4 A B C D.
 
-notation < "a ∧ b ∧ c ∧ d" left associative with precedence 60 for @{'and3 $a $b $c $d}.
+notation < "a ∧ b ∧ c ∧ d" left associative with precedence 35 for @{'and4 $a $b $c $d}.
  
 interpretation "constructive quaternary and" 'and4 x y z t = (Conj4 x y z t).
 
@@ -47,28 +47,35 @@ interpretation "CProp exists" 'exists \eta.x = (exT _ x).
 inductive exT23 (A:Type) (P:A→CProp) (Q:A→CProp) (R:A→A→CProp) : CProp ≝
   ex_introT23: ∀w,p:A. P w → Q p → R w p → exT23 A P Q R.
 
-notation < "'fst' \nbsp x" non associative with precedence 50 for @{'pi1 $x}.
-notation < "'snd' \nbsp x" non associative with precedence 50 for @{'pi2 $x}.
-notation > "'fst' x" non associative with precedence 50 for @{'pi1 $x}.
-notation > "'snd' x" non associative with precedence 50 for @{'pi2 $x}.
-notation < "'fst' \nbsp x \nbsp y" non associative with precedence 50 for @{'pi12 $x $y}.
-notation < "'snd' \nbsp x \nbsp y" non associative with precedence 50 for @{'pi22 $x $y}.
+notation < "'fst' \nbsp x" non associative with precedence 90 for @{'pi1a $x}.
+notation < "'snd' \nbsp x" non associative with precedence 90 for @{'pi2a $x}.
+notation < "'fst' \nbsp x \nbsp y" non associative with precedence 90 for @{'pi1b $x $y}.
+notation < "'snd' \nbsp x \nbsp y" non associative with precedence 90 for @{'pi2b $x $y}.
+notation > "'fst'" non associative with precedence 90 for @{'pi1}.
+notation > "'snd'" non associative with precedence 90 for @{'pi2}.
 
 definition pi1exT ≝ λA,P.λx:exT A P.match x with [ex_introT x _ ⇒ x].
+definition pi2exT ≝ 
+  λA,P.λx:exT A P.match x return λx.P (pi1exT ?? x) with [ex_introT _ p ⇒ p].
 
-interpretation "exT fst" 'pi1 x = (pi1exT _ _ x).
-interpretation "exT fst 2" 'pi12 x y = (pi1exT _ _ x y).
+interpretation "exT fst" 'pi1 = (pi1exT _ _).
+interpretation "exT fst" 'pi1a x = (pi1exT _ _ x).
+interpretation "exT fst" 'pi1b x y = (pi1exT _ _ x y).
+interpretation "exT snd" 'pi2 = (pi2exT _ _).
+interpretation "exT snd" 'pi2a x = (pi2exT _ _ x).
+interpretation "exT snd" 'pi2b x y = (pi2exT _ _ x y).
 
 definition pi1exT23 ≝
   λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 x _ _ _ _ ⇒ x].
 definition pi2exT23 ≝
   λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 _ x _ _ _ ⇒ x].
-   
-interpretation "exT2 fst" 'pi1 x = (pi1exT23 _ _ _ _ x).
-interpretation "exT2 snd" 'pi2 x = (pi2exT23 _ _ _ _ x).
-interpretation "exT2 fst 2" 'pi12 x y = (pi1exT23 _ _ _ _ x y).
-interpretation "exT2 snd 2" 'pi22 x y = (pi2exT23 _ _ _ _ x y).
 
+interpretation "exT2 fst" 'pi1 = (pi1exT23 _ _ _ _).
+interpretation "exT2 snd" 'pi2 = (pi2exT23 _ _ _ _).   
+interpretation "exT2 fst" 'pi1a x = (pi1exT23 _ _ _ _ x).
+interpretation "exT2 snd" 'pi2a x = (pi2exT23 _ _ _ _ x).
+interpretation "exT2 fst" 'pi1b x y = (pi1exT23 _ _ _ _ x y).
+interpretation "exT2 snd" 'pi2b x y = (pi2exT23 _ _ _ _ x y).
 
 definition Not : CProp → Prop ≝ λx:CProp.x → False.
 
diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends
index 368625b80..d00e75e49 100644
--- a/helm/software/matita/contribs/dama/dama/depends
+++ b/helm/software/matita/contribs/dama/dama/depends
@@ -4,17 +4,16 @@ uniform.ma supremum.ma
 bishop_set.ma ordered_set.ma
 sequence.ma nat/nat.ma
 ordered_uniform.ma uniform.ma
-supremum.ma bishop_set.ma cprop_connectives.ma nat/plus.ma nat_ordered_set.ma ordered_set.ma sequence.ma
+supremum.ma bishop_set.ma cprop_connectives.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma ordered_set.ma sequence.ma
 property_exhaustivity.ma ordered_uniform.ma property_sigma.ma
 bishop_set_rewrite.ma bishop_set.ma
 cprop_connectives.ma logic/equality.ma
-nat_ordered_set.ma cprop_connectives.ma nat/compare.ma ordered_set.ma
+nat_ordered_set.ma ordered_set.ma bishop_set.ma cprop_connectives.ma nat/compare.ma
 lebesgue.ma property_exhaustivity.ma sandwich.ma
 ordered_set.ma cprop_connectives.ma
 russell_support.ma cprop_connectives.ma nat/nat.ma
-models/uniformnat.ma bishop_set_rewrite.ma datatypes/constructors.ma decidable_kit/decidable.ma nat_ordered_set.ma ordered_uniform.ma russell_support.ma uniform.ma
+models/uniformnat.ma bishop_set_rewrite.ma nat_ordered_set.ma ordered_uniform.ma russell_support.ma uniform.ma
 datatypes/constructors.ma 
-decidable_kit/decidable.ma 
 logic/equality.ma 
 nat/compare.ma 
 nat/nat.ma 
diff --git a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
index 18ecf8e60..d625d391d 100644
--- a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
@@ -12,9 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "bishop_set.ma". 
 include "nat/compare.ma".
-include "cprop_connectives.ma".
+include "bishop_set.ma". 
 
 definition nat_excess : nat → nat → CProp ≝ λn,m. m<n.
 
@@ -26,6 +25,7 @@ intros 5;elim n; [apply H]
 cases m;[ apply H1| apply H2; apply H3 ]
 qed.
 
+alias symbol "lt" = "natural 'less than'".
 lemma nat_discriminable: ∀x,y:nat.x < y ∨ x = y ∨ y < x.
 intros (x y); apply (nat_elim2 ???? x y); 
 [1: intro;left;cases n; [right;reflexivity] left; apply lt_O_S;
@@ -49,18 +49,17 @@ apply (mk_ordered_set ? nat_excess);
 |2: apply nat_excess_cotransitive]
 qed.
 
-alias id "le" = "cic:/matita/dama/ordered_set/le.con".
+alias id "le" = "cic:/matita/nat/orders/le.ind#xpointer(1/1)".
 lemma os_le_to_nat_le:
-  ∀a,b:nat_ordered_set.le nat_ordered_set a b → a ≤ b.
+  ∀a,b:nat_ordered_set.a ≤ b → le a b.
 intros; normalize in H; apply (not_lt_to_le ?? H);
 qed.
  
 lemma nat_le_to_os_le:
-  ∀a,b:nat_ordered_set.a ≤ b → le nat_ordered_set a b.
+  ∀a,b:nat_ordered_set.le a b → a ≤ b.
 intros 3; apply (le_to_not_lt a b);assumption;
 qed.
 
-alias id "lt" = "cic:/matita/dama/bishop_set/lt.con".
 lemma nat_lt_to_os_lt:
   ∀a,b:nat_ordered_set.a < b → lt nat_ordered_set a b.
 intros 3; split;
diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
index 1ca01611f..c9b5e7da6 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
@@ -38,7 +38,8 @@ record ordered_uniform_space : Type ≝ {
 }.   
 
 lemma segment_square_of_O_square: 
-  ∀O:ordered_set.∀u,v:O.∀x:O square.fst x ∈ [u,v] → snd x ∈ [u,v] → {[u,v]} square.
+  ∀O:ordered_set.∀u,v:O.∀x:O square.
+   fst x ∈ [u,v] → snd x ∈ [u,v] → {[u,v]} square.
 intros; split; exists; [1: apply (fst x) |3: apply (snd x)] assumption;
 qed.
 
diff --git a/helm/software/matita/contribs/dama/dama/sequence.ma b/helm/software/matita/contribs/dama/dama/sequence.ma
index 3bcb691a5..482e8aed7 100644
--- a/helm/software/matita/contribs/dama/dama/sequence.ma
+++ b/helm/software/matita/contribs/dama/dama/sequence.ma
@@ -14,8 +14,24 @@
 
 include "nat/nat.ma".
 
-definition sequence := λO:Type.nat → O.
+inductive sequence (O:Type) : Type ≝  
+ | mk_seq : (nat → O) → sequence O.
 
-definition fun_of_sequence: ∀O:Type.sequence O → nat → O ≝ λO.λx:sequence O.x.
+definition fun_of_seq: ∀O:Type.sequence O → nat → O ≝ 
+  λO.λx:sequence O.match x with [ mk_seq f ⇒ f ].
 
-coercion cic:/matita/dama/sequence/fun_of_sequence.con 1.
+coercion cic:/matita/dama/sequence/fun_of_seq.con 1.
+
+notation < "hvbox((\lfloor p \rfloor) \sub ident i)"
+  left associative with precedence 70
+for @{ 'sequence (\lambda ${ident i} : $t . $p)}.
+
+notation > "hvbox(\lfloor ident i, p \rfloor)"
+  left associative with precedence 70
+for @{ 'sequence (\lambda ${ident i} . $p)}.
+  
+notation "a \sub i" left associative with precedence 70 
+  for @{ 'sequence_appl $a $i }.
+
+interpretation "sequence" 'sequence \eta.x = (mk_seq _ x).
+interpretation "sequence element" 'sequence_appl s i = (fun_of_seq _ s i).
diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index e6b9dbbc6..ea5c55050 100644
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -12,9 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "sequence.ma".
-include "ordered_set.ma".
+
 include "datatypes/constructors.ma".
+include "nat/plus.ma".
+include "nat_ordered_set.ma".
+include "sequence.ma".
 
 (* Definition 2.4 *)
 definition upper_bound ≝ λO:ordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
@@ -28,40 +30,38 @@ definition infimum ≝
 definition increasing ≝ λO:ordered_set.λa:sequence O.∀n:nat.a n ≤ a (S n).
 definition decreasing ≝ λO:ordered_set.λa:sequence O.∀n:nat.a (S n) ≤ a n.
 
-notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50 
+notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 45 
   for @{'upper_bound $s $x}.
-notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 50 
+notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 45 
   for @{'lower_bound $s $x}.
-notation < "s \nbsp 'is_increasing'" non associative with precedence 50 
+notation < "s \nbsp 'is_increasing'" non associative with precedence 45 
   for @{'increasing $s}.
-notation < "s \nbsp 'is_decreasing'" non associative with precedence 50 
+notation < "s \nbsp 'is_decreasing'" non associative with precedence 45 
   for @{'decreasing $s}.
-notation < "x \nbsp 'is_supremum' \nbsp s" non associative with precedence 50 
+notation < "x \nbsp 'is_supremum' \nbsp s" non associative with precedence 45 
   for @{'supremum $s $x}.
-notation < "x \nbsp 'is_infimum' \nbsp s" non associative with precedence 50 
+notation < "x \nbsp 'is_infimum' \nbsp s" non associative with precedence 45 
   for @{'infimum $s $x}.
 
-notation > "x 'is_upper_bound' s" non associative with precedence 50 
+notation > "x 'is_upper_bound' s" non associative with precedence 45 
   for @{'upper_bound $s $x}.
-notation > "x 'is_lower_bound' s" non associative with precedence 50 
+notation > "x 'is_lower_bound' s" non associative with precedence 45 
   for @{'lower_bound $s $x}.
-notation > "s 'is_increasing'"    non associative with precedence 50 
+notation > "s 'is_increasing'"    non associative with precedence 45 
   for @{'increasing $s}.
-notation > "s 'is_decreasing'"    non associative with precedence 50 
+notation > "s 'is_decreasing'"    non associative with precedence 45 
   for @{'decreasing $s}.
-notation > "x 'is_supremum' s"  non associative with precedence 50 
+notation > "x 'is_supremum' s"  non associative with precedence 45 
   for @{'supremum $s $x}.
-notation > "x 'is_infimum' s"  non associative with precedence 50 
+notation > "x 'is_infimum' s"  non associative with precedence 45 
   for @{'infimum $s $x}.
 
 interpretation "Ordered set upper bound" 'upper_bound s x = (upper_bound _ s x).
 interpretation "Ordered set lower bound" 'lower_bound s x = (lower_bound _ s x).
-interpretation "Ordered set increasing"  'increasing s    = (increasing _ s).
-interpretation "Ordered set decreasing"  'decreasing s    = (decreasing _ s).
-interpretation "Ordered set strong sup"  'supremum s x  = (supremum _ s x).
-interpretation "Ordered set strong inf"  'infimum s x  = (infimum _ s x).
-  
-include "bishop_set.ma".
+interpretation "Ordered set increasing"  'increasing s = (increasing _ s).
+interpretation "Ordered set decreasing"  'decreasing s = (decreasing _ s).
+interpretation "Ordered set strong sup"  'supremum s x = (supremum _ s x).
+interpretation "Ordered set strong inf"  'infimum s x = (infimum _ s x).
   
 lemma uniq_supremum: 
   ∀O:ordered_set.∀s:sequence O.∀t1,t2:O.
@@ -87,14 +87,12 @@ intros 7 (C s u Hu v Hv H); cases Hu (_ H1); clear Hu;
 cases (H1 ? H) (w Hw); apply Hv; assumption;
 qed.
 
-
 (* Lemma 2.6 *)
 definition strictly_increasing ≝ 
   λC:ordered_set.λa:sequence C.∀n:nat.a (S n) ≰ a n.
 definition strictly_decreasing ≝ 
   λC:ordered_set.λa:sequence C.∀n:nat.a n ≰ a (S n).
 
- 
 notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 50 
   for @{'strictly_increasing $s}.
 notation > "s 'is_strictly_increasing'" non associative with precedence 50 
@@ -116,21 +114,17 @@ definition downarrow ≝
   λC:ordered_set.λs:sequence C.λu:C.
    s is_decreasing ∧ u is_infimum s.
      
-notation < "a \uparrow \nbsp u" non associative with precedence 50 for @{'sup_inc $a $u}.
-notation > "a \uparrow u" non associative with precedence 50 for @{'sup_inc $a $u}.
+notation < "a \uparrow \nbsp u" non associative with precedence 45 for @{'sup_inc $a $u}.
+notation > "a \uparrow u" non associative with precedence 45 for @{'sup_inc $a $u}.
 interpretation "Ordered set uparrow" 'sup_inc s u = (uparrow _ s u).
 
-notation < "a \downarrow \nbsp u" non associative with precedence 50 for @{'inf_dec $a $u}.
-notation > "a \downarrow u" non associative with precedence 50 for @{'inf_dec $a $u}.
+notation < "a \downarrow \nbsp u" non associative with precedence 45 for @{'inf_dec $a $u}.
+notation > "a \downarrow u" non associative with precedence 45 for @{'inf_dec $a $u}.
 interpretation "Ordered set downarrow" 'inf_dec s u = (downarrow _ s u).
 
-include "nat/plus.ma".
-include "nat_ordered_set.ma".
-  
-alias symbol "nleq" = "Ordered set excess".
-alias symbol "leq" = "Ordered set less or equal than".
 lemma trans_increasing: 
-  ∀C:ordered_set.∀a:sequence C.a is_increasing → ∀n,m:nat_ordered_set. n ≤ m → a n ≤ a m.
+  ∀C:ordered_set.∀a:sequence C.a is_increasing → 
+   ∀n,m:nat_ordered_set. n ≤ m → a n ≤ a m.
 intros 5 (C a Hs n m); elim m; [
   rewrite > (le_n_O_to_eq n (not_lt_to_le O n H));
   intro X; cases (os_coreflexive ?? X);]
@@ -141,7 +135,8 @@ cases (le_to_or_lt_eq ?? (not_lt_to_le (S n1) n H1)); clear H1;
 qed.
 
 lemma trans_decreasing: 
-  ∀C:ordered_set.∀a:sequence C.a is_decreasing → ∀n,m:nat_ordered_set. n ≤ m → a m ≤ a n.
+  ∀C:ordered_set.∀a:sequence C.a is_decreasing → 
+   ∀n,m:nat_ordered_set. n ≤ m → a m ≤ a n.
 intros 5 (C a Hs n m); elim m; [
   rewrite > (le_n_O_to_eq n (not_lt_to_le O n H));
   intro X; cases (os_coreflexive ?? X);]
@@ -152,7 +147,8 @@ cases (le_to_or_lt_eq ?? (not_lt_to_le (S n1) n H1)); clear H1;
 qed.
 
 lemma trans_increasing_exc: 
-  ∀C:ordered_set.∀a:sequence C.a is_increasing → ∀n,m:nat_ordered_set. m ≰ n → a n ≤ a m.
+  ∀C:ordered_set.∀a:sequence C.a is_increasing → 
+   ∀n,m:nat_ordered_set. m ≰ n → a n ≤ a m.
 intros 5 (C a Hs n m); elim m; [cases (not_le_Sn_O n H);]
 intro; apply H; 
 [1: change in n1 with (os_carr nat_ordered_set); (* canonical structures *) 
@@ -164,7 +160,8 @@ intro; apply H;
 qed.
 
 lemma trans_decreasing_exc: 
-  ∀C:ordered_set.∀a:sequence C.a is_decreasing → ∀n,m:nat_ordered_set. m ≰ n → a m ≤ a n .
+  ∀C:ordered_set.∀a:sequence C.a is_decreasing →
+   ∀n,m:nat_ordered_set. m ≰ n → a m ≤ a n .
 intros 5 (C a Hs n m); elim m; [cases (not_le_Sn_O n H);]
 intro; apply H; 
 [1: change in n1 with (os_carr nat_ordered_set); (* canonical structures *) 
@@ -175,6 +172,7 @@ intro; apply H;
     cases (Hs n1); assumption;]
 qed.
 
+alias symbol "exists" = "CProp exists".
 lemma strictly_increasing_reaches: 
   ∀C:ordered_set.∀m:sequence nat_ordered_set.
    m is_strictly_increasing → ∀w.∃t.m t ≰ w.
@@ -193,7 +191,7 @@ qed.
      
 lemma selection_uparrow: 
   ∀C:ordered_set.∀m:sequence nat_ordered_set.m is_strictly_increasing →
-    ∀a:sequence C.∀u.a ↑ u → (λx.a (m x)) ↑ u.
+    ∀a:sequence C.∀u.a ↑ u → ⌊x,a (m x)⌋ ↑ u.
 intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split; 
 [1: intro n; simplify; apply trans_increasing_exc; [assumption] apply (Hm n);
 |2: intro n; simplify; apply Uu;
@@ -205,7 +203,7 @@ qed.
 
 lemma selection_downarrow: 
   ∀C:ordered_set.∀m:sequence nat_ordered_set.m is_strictly_increasing →
-    ∀a:sequence C.∀u.a ↓ u → (λx.a (m x)) ↓ u.
+    ∀a:sequence C.∀u.a ↓ u → ⌊x,a (m x)⌋ ↓ u.
 intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split; 
 [1: intro n; simplify; apply trans_decreasing_exc; [assumption] apply (Hm n);
 |2: intro n; simplify; apply Uu;
@@ -213,42 +211,41 @@ intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split;
     cases (strictly_increasing_reaches C ? Hm w); 
     exists [apply w1]; cases (os_cotransitive ??? (a (m w1)) H); [assumption]  
     cases (trans_decreasing_exc C ? Ia ?? H1); assumption;]
-qed.     
+qed.
 
 (* Definition 2.7 *)
-alias id "ExT23" = "cic:/matita/dama/cprop_connectives/exT23.ind#xpointer(1/1)".
 definition order_converge ≝
   λO:ordered_set.λa:sequence O.λx:O.
    ExT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
-     (λl,u.∀i:nat. (l i) is_infimum (λw.a (w+i)) ∧ (u i) is_supremum (λw.a (w+i))).
+     (λl,u.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧ 
+                   (u i) is_supremum ⌊w,a (w+i)⌋).
     
-notation < "a \nbsp (\circ \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50 
+notation < "a \nbsp (\circ \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45 
   for @{'order_converge $a $x}.
-notation > "a 'order_converges' x" non associative with precedence 50 
+notation > "a 'order_converges' x" non associative with precedence 45 
   for @{'order_converge $a $x}.
 interpretation "Order convergence" 'order_converge s u = (order_converge _ s u).   
     
 (* Definition 2.8 *)
+alias symbol "and" = "constructive and".
+definition segment ≝ λO:ordered_set.λa,b:O.λx:O.(x ≤ b) ∧ (a ≤ x).
 
-definition segment ≝ λO:ordered_set.λa,b:O.λx:O.
-  (cic:/matita/logic/connectives/And.ind#xpointer(1/1) (x ≤ b) (a ≤ x)).
-
-notation "[a,b]" non associative with precedence 50 
-  for @{'segment $a $b}.
+notation "[a,b]" left associative with precedence 70 for @{'segment $a $b}.
 interpretation "Ordered set sergment" 'segment a b = (segment _ a b).
 
-notation "hvbox(x \in break [a,b])" non associative with precedence 50 
-  for @{'segment2 $a $b $x}.
-interpretation "Ordered set sergment in" 'segment2 a b x= (segment _ a b x).
+notation "hvbox(x \in break [a,b])" non associative with precedence 45 
+  for @{'segment_in $a $b $x}.
+interpretation "Ordered set sergment in" 'segment_in a b x= (segment _ a b x).
 
+(*
 coinductive sigma (A:Type) (P:A→Prop) : Type ≝ sig_in : ∀x.P x → sigma A P.
 
-definition pi1 : ∀A.∀P.sigma A P → A ≝ λA,P,s.match s with [sig_in x _ ⇒ x].  
+definition pi1sig : ∀A.∀P.sigma A P → A ≝ λA,P,s.match s with [sig_in x _ ⇒ x].  
 
-interpretation "sigma pi1" 'pi1 x = (pi1 _ _ x).
+interpretation "sigma pi1" 'pi1a x = (pi1sig _ _ x).
  
-interpretation "Type exists" 'exists \eta.x =
-  (cic:/matita/dama/supremum/sigma.ind#xpointer(1/1) _ x).
+interpretation "Type exists" 'exists \eta.x = (sigma _ x).
+*)
 
 lemma segment_ordered_set: 
   ∀O:ordered_set.∀u,v:O.ordered_set.
@@ -258,16 +255,16 @@ intros (O u v); apply (mk_ordered_set (∃x.x ∈ [u,v]));
 |3: intros 3 (x y z); cases x; cases y ; cases z; simplify; apply os_cotransitive]
 qed.
 
-notation "hvbox({[a, break b]})" non associative with precedence 80 
+notation "hvbox({[a, break b]})" non associative with precedence 90 
   for @{'segment_set $a $b}.
 interpretation "Ordered set segment" 'segment_set a b = 
- (segment_ordered_set _ a b).
+  (segment_ordered_set _ a b).
 
 (* Lemma 2.9 *)
 lemma segment_preserves_supremum:
   ∀O:ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}. 
-    (λn.fst (a n)) is_increasing ∧ 
-    (fst x) is_supremum (λn.fst (a n)) → a ↑ x.
+    ⌊n,fst (a n)⌋ is_increasing ∧ 
+    (fst x) is_supremum ⌊n,fst (a n)⌋ → a ↑ x.
 intros; split; cases H; clear H; 
 [1: apply H1;
 |2: cases H2; split; clear H2;
@@ -277,8 +274,8 @@ qed.
 
 lemma segment_preserves_infimum:
   ∀O:ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}. 
-    (λn.fst (a n)) is_decreasing ∧ 
-    (fst x) is_infimum (λn.fst (a n)) → a ↓ x.
+    ⌊n,fst (a n)⌋ is_decreasing ∧ 
+    (fst x) is_infimum ⌊n,fst (a n)⌋ → a ↓ x.
 intros; split; cases H; clear H; 
 [1: apply H1;
 |2: cases H2; split; clear H2;
@@ -286,20 +283,22 @@ intros; split; cases H; clear H;
     |2: clear H; intro y0; apply (H3 (fst y0));]]
 qed.
 
-
 (* Definition 2.10 *)
 coinductive pair (A,B:Type) : Type ≝ prod : ∀a:A.∀b:B.pair A B. 
 definition first : ∀A.∀P.pair A P → A ≝ λA,P,s.match s with [prod x _ ⇒ x].
 definition second : ∀A.∀P.pair A P → P ≝ λA,P,s.match s with [prod _ y ⇒ y].
-  
-interpretation "pair pi1" 'pi1 x = (first _ _ x).
-interpretation "pair pi2" 'pi2 x = (second _ _ x).
 
-notation "hvbox(\langle a, break b\rangle)" non associative with precedence 91 for @{ 'pair $a $b}.
+interpretation "pair pi1" 'pi1 = (first _ _).
+interpretation "pair pi2" 'pi2 = (second _ _).
+interpretation "pair pi1" 'pi1a x = (first _ _ x).
+interpretation "pair pi2" 'pi2a x = (second _ _ x).
+interpretation "pair pi1" 'pi1b x y = (first _ _ x y).
+interpretation "pair pi2" 'pi2b x y = (second _ _ x y).
+
+notation "hvbox(\langle a, break b\rangle)" left associative with precedence 70 for @{ 'pair $a $b}.
 interpretation "pair" 'pair a b = (prod _ _ a b).
- 
 interpretation "prod" 'product a b = (pair a b).
- 
+
 lemma square_ordered_set: ordered_set → ordered_set.
 intro O;
 apply (mk_ordered_set (O × O));
@@ -312,7 +311,7 @@ apply (mk_ordered_set (O × O));
     |2: cases (os_cotransitive ??? z2 H1); [left;right|right;right]assumption]]
 qed.
 
-notation < "s  2 \atop \nleq" non associative with precedence 90
+notation < "s 2 \atop \nleq" non associative with precedence 90
   for @{ 'square $s }.
 notation > "s 'square'" non associative with precedence 90
   for @{ 'square $s }.
@@ -320,13 +319,11 @@ interpretation "ordered set square" 'square s = (square_ordered_set s).
  
 definition square_segment ≝ 
   λO:ordered_set.λa,b:O.λx:square_ordered_set O.
-  (cic:/matita/logic/connectives/And.ind#xpointer(1/1)
-   (cic:/matita/logic/connectives/And.ind#xpointer(1/1) (fst x ≤ b) (a ≤ fst x))
-   (cic:/matita/logic/connectives/And.ind#xpointer(1/1) (snd x ≤ b) (a ≤ snd x))).
+    And4 (fst x ≤ b) (a ≤ fst x) (snd x ≤ b) (a ≤ snd x).
  
 definition convex ≝
   λO:ordered_set.λU:O square → Prop.
-  ∀p.U p → fst p ≤ snd p → ∀y. square_segment ? (fst p) (snd p) y → U y.
+    ∀p.U p → fst p ≤ snd p → ∀y. square_segment ? (fst p) (snd p) y → U y.
   
 (* Definition 2.11 *)  
 definition upper_located ≝
@@ -337,18 +334,18 @@ definition lower_located ≝
   λO:ordered_set.λa:sequence O.∀x,y:O. x ≰ y → 
     (∃i:nat.x ≰ a i) ∨ (∃b:O.b≰y ∧ ∀i:nat.b ≤ a i).
 
-notation < "s \nbsp 'is_upper_located'" non associative with precedence 50 
+notation < "s \nbsp 'is_upper_located'" non associative with precedence 45 
   for @{'upper_located $s}.
-notation > "s 'is_upper_located'" non associative with precedence 50 
+notation > "s 'is_upper_located'" non associative with precedence 45 
   for @{'upper_located $s}.
-interpretation "Ordered set upper locatedness" 'upper_located s    = 
+interpretation "Ordered set upper locatedness" 'upper_located s = 
   (upper_located _ s).
 
-notation < "s \nbsp 'is_lower_located'" non associative with precedence 50 
+notation < "s \nbsp 'is_lower_located'" non associative with precedence 45 
   for @{'lower_located $s}.
-notation > "s 'is_lower_located'" non associative with precedence 50 
+notation > "s 'is_lower_located'" non associative with precedence 45
   for @{'lower_located $s}.
-interpretation "Ordered set lower locatedness" 'lower_located s    = 
+interpretation "Ordered set lower locatedness" 'lower_located s = 
   (lower_located _ s).
     
 (* Lemma 2.12 *)    
diff --git a/helm/software/matita/contribs/dama/dama/uniform.ma b/helm/software/matita/contribs/dama/dama/uniform.ma
index 348b99a81..b8b77572b 100644
--- a/helm/software/matita/contribs/dama/dama/uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/uniform.ma
@@ -31,11 +31,6 @@ notation "a \subseteq u" left associative with precedence 70
   for @{ 'subset $a $u }.
 interpretation "Bishop subset" 'subset a b = (subset _ a b). 
 
-notation "hvbox({ ident x : t | break p })" non associative with precedence 80
-  for @{ 'explicitset (\lambda ${ident x} : $t . $p) }.  
-definition mk_set ≝ λT:bishop_set.λx:T→Prop.x.
-interpretation "explicit set" 'explicitset t = (mk_set _ t).
-
 notation < "s  2 \atop \neq" non associative with precedence 90
   for @{ 'square2 $s }.
 notation > "s 'square'" non associative with precedence 90
@@ -43,44 +38,41 @@ notation > "s 'square'" non associative with precedence 90
 interpretation "bishop set square" 'square x = (square_bishop_set x).    
 interpretation "bishop set square" 'square2 x = (square_bishop_set x).    
 
-
 alias symbol "exists" = "exists".
 alias symbol "and" = "logical and".
 definition compose_relations ≝
   λC:bishop_set.λU,V:C square → Prop.
    λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉.
    
-notation "a \circ b"  left associative with precedence 60
+notation "a \circ b"  left associative with precedence 70
   for @{'compose $a $b}.
 interpretation "relations composition" 'compose a b = (compose_relations _ a b).
-notation "hvbox(x \in break a \circ break b)"  non associative with precedence 50
-  for @{'compose2 $a $b $x}.
-interpretation "relations composition" 'compose2 a b x = 
- (compose_relations _ a b x).
 
 definition invert_relation ≝
   λC:bishop_set.λU:C square → Prop.
     λx:C square. U 〈snd x,fst x〉.
     
-notation < "s \sup (-1)"  non associative with precedence 90
+notation < "s \sup (-1)"  left associative with precedence 70
   for @{ 'invert $s }.
-notation < "s \sup (-1) x"  non associative with precedence 90
+notation < "s \sup (-1) x"  left associative with precedence 70
   for @{ 'invert2 $s $x}. 
-notation > "'inv' s" non associative with precedence 90
-  for @{ 'invert $s }.
+notation > "'inv'" right associative with precedence 70
+  for @{ 'invert0  }.
 interpretation "relation invertion" 'invert a = (invert_relation _ a).
+interpretation "relation invertion" 'invert0 = (invert_relation _).
 interpretation "relation invertion" 'invert2 a x = (invert_relation _ a x).
 
 alias symbol "exists" = "CProp exists".
-alias symbol "and" (instance 18) = "constructive and".
-alias symbol "and" (instance 10) = "constructive and".
+alias symbol "and" (instance 21) = "constructive and".
+alias symbol "and" (instance 16) = "constructive and".
+alias symbol "and" (instance 9) = "constructive and".
 record uniform_space : Type ≝ {
   us_carr:> bishop_set;
   us_unifbase: (us_carr square → Prop) → CProp;
   us_phi1: ∀U:us_carr square → Prop. us_unifbase U → 
-    {x:us_carr square|fst x ≈ snd x} ⊆ U;
+    (λx:us_carr square.fst x ≈ snd x) ⊆ U;
   us_phi2: ∀U,V:us_carr square → Prop. us_unifbase U → us_unifbase V →
-    ∃W:us_carr square → Prop.us_unifbase W ∧ (W ⊆ {x:?|U x ∧ V x});
+    ∃W:us_carr square → Prop.us_unifbase W ∧ (W ⊆ (λx.U x ∧ V x));
   us_phi3: ∀U:us_carr square → Prop. us_unifbase U → 
     ∃W:us_carr square → Prop.us_unifbase W ∧ (W ∘ W) ⊆ U;
   us_phi4: ∀U:us_carr square → Prop. us_unifbase U → ∀x.(U x → (inv U) x) ∧ ((inv U) x → U x)
@@ -121,12 +113,3 @@ apply H; unfold; exists [apply x]; split [2: apply (Hn ? H2)]
 cases (us_phi4 ?? Hv 〈a i,x〉) (P1 P2); apply P2;
 apply (Hn ? H1);
 qed.
-
-(* Definition 2.17 *)
-definition mk_big_set ≝
-  λP:CProp.λF:P→CProp.F.
-interpretation "explicit big set" 'explicitset t = (mk_big_set _ t).
-    
-definition restrict_uniformity ≝
-  λC:uniform_space.λX:C→Prop.
-   {U:C square → Prop| (U ⊆ {x:C square|X (fst x) ∧ X(snd x)}) ∧ us_unifbase C U}.