Since CProp_i = Type_i everything lowered without 2 distinct Sigma.

diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
index bd528521dba3e8ea456a501256f8f5f93ef91800..93fbac9b287770fa803cc9865c371bdf60c658e9 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
+++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
@@ -61,27 +61,12 @@ interpretation "constructive quaternary and" 'and4 x y z t = (And4 x y z t).
 
 inductive exT (A:Type) (P:A→CProp) : CProp ≝
   ex_introT: ∀w:A. P w → exT A P.
-
-record sigT (A:Type) (P:A→Prop) : Type ≝ {
-  fstT:A;
-  sndT:P fstT
-}.
   
-interpretation "sigT \fst" 'pi1 = (fstT _ _).
-interpretation "sigT \fst" 'pi1a x = (fstT _ _ x).
-interpretation "sigT \fst" 'pi1b x y = (fstT _ _ x y).
-interpretation "sigT \snd" 'pi2 = (sndT _ _).
-interpretation "sigT \snd" 'pi2a x = (sndT _ _ x).
-interpretation "sigT \snd" 'pi2b x y = (sndT _ _ x y).
-
 notation "\ll term 19 a, break term 19 b \gg" 
 with precedence 90 for @{'dependent_pair $a $b}.
 interpretation "dependent pair" 'dependent_pair a b = 
   (ex_introT _ _ a b).
 
-interpretation "dependent set" 'dependent_pair a b = 
-  (mk_sigT _ _ a b).
-
 interpretation "CProp exists" 'exists \eta.x = (exT _ x).
 
 notation "\ll term 19 a, break term 19 b \gg" 

diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma
index 6daebfa0cde944051d1b03fe7d2ddd35cd415d3e..d0fcae691b5acd7fe38626411d1e70b87afd1690 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma
@@ -65,10 +65,10 @@ split;
     [1: apply (le_transitive ???? (H8 0)); cases (Hyi 0); assumption
     |2: apply (le_transitive ????? (H4 0)); cases (Hxi 0); assumption]
 |2: intros 3 (h);
-    letin Xi ≝ (⌊n,mk_sigT ?? (xi n) (Hxi n)⌋);
-    letin Yi ≝ (⌊n,mk_sigT ?? (yi n) (Hyi n)⌋);
-    letin Ai ≝ (⌊n,mk_sigT ?? (a n) (H1 n)⌋);
-    apply (sandwich {[l,u]} (mk_sigT ?? x h) Xi Yi Ai); try assumption;
+    letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋);
+    letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋);
+    letin Ai ≝ (⌊n,≪a n, H1 n≫⌋);
+    apply (sandwich {[l,u]} ≪?, h≫ Xi Yi Ai); try assumption;
     [1: intro j; cases (Hxy j); cases H3; cases H4; split;
         [apply (H5 0);|apply (H7 0)]
     |2: cases (H l u Xi ≪?,h≫) (Ux Uy); apply Ux; cases Hx; split; [apply H3;]
@@ -108,10 +108,10 @@ split;
 |2: intros 3;
     lapply (uparrow_upperlocated ? xi x Hx)as Ux;
     lapply (downarrow_lowerlocated ? yi x Hy)as Uy;
-    letin Xi ≝ (⌊n,mk_sigT ?? (xi n) (Hxi n)⌋);
-    letin Yi ≝ (⌊n,mk_sigT ?? (yi n) (Hyi n)⌋);
-    letin Ai ≝ (⌊n,mk_sigT ?? (a n) (H1 n)⌋);
-    apply (sandwich {[l,u]} (mk_sigT ?? x h) Xi Yi Ai); try assumption;
+    letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋);
+    letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋);
+    letin Ai ≝ (⌊n,≪a n, H1 n≫⌋);
+    apply (sandwich {[l,u]} ≪?, h≫ Xi Yi Ai); try assumption;
     [1: intro j; cases (Hxy j); cases H3; cases H4; split;
         [apply (H5 0);|apply (H7 0)]
     |2: cases (restrict_uniform_convergence_uparrow ? S ?? (H l u) Xi x Hx);

diff --git a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
index 7bb312aff0284a0a6bef069af9d5fe19e4115a18..b5610cbe0de1e82014050350e42855e77ee6eef7 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
+++ b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
@@ -17,7 +17,7 @@ include "supremum.ma".
 include "nat/le_arith.ma".
 include "russell_support.ma".
 
-alias symbol "pi1" = "sigT \fst".
+alias symbol "pi1" = "exT \fst".
 alias symbol "leq" = "natural 'less or equal to'".
 lemma nat_dedekind_sigma_complete:
   ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing → 
@@ -114,7 +114,7 @@ apply le_to_le_to_eq;
     rewrite < (H4 ?); [2: reflexivity] apply le_n;]
 qed.
 
-alias symbol "pi1" = "sigT \fst".
+alias symbol "pi1" = "exT \fst".
 alias symbol "leq" = "natural 'less or equal to'".
 alias symbol "nat" = "ordered set N".
 axiom nat_dedekind_sigma_complete_r:

diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
index 2ffda533ac61a612f850eb103d3b2e6e81b1473d..66bcf6f0bf4595b1f346491113b8bac56586c316 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
@@ -30,7 +30,7 @@ unfold bishop_set_OF_ordered_uniform_space_;
 |5: cases (with_ X); simplify; apply (us_phi4 (ous_us_ X))]
 qed.
 
-coercion cic:/matita/dama/ordered_uniform/ous_unifspace.con.
+coercion ous_unifspace.
 
 record ordered_uniform_space : Type ≝ {
   ous_stuff :> ordered_uniform_space_;
@@ -51,15 +51,15 @@ lemma segment_square_of_ordered_set_square:
 intros; split; exists; [1: apply (\fst x) |3: apply (\snd x)] assumption;
 qed.
 
-coercion cic:/matita/dama/ordered_uniform/segment_square_of_ordered_set_square.con 0 2.
+coercion segment_square_of_ordered_set_square with 0 2.
 
-alias symbol "pi1" (instance 4) = "sigT \fst".
-alias symbol "pi1" (instance 2) = "sigT \fst".
+alias symbol "pi1" (instance 4) = "exT \fst".
+alias symbol "pi1" (instance 2) = "exT \fst".
 lemma ordered_set_square_of_segment_square : 
  ∀O:ordered_set.∀u,v:O.{[u,v]} square → O square ≝ 
   λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈\fst(\fst b),\fst(\snd b)〉.
 
-coercion cic:/matita/dama/ordered_uniform/ordered_set_square_of_segment_square.con.
+coercion ordered_set_square_of_segment_square.
 
 lemma restriction_agreement : 
   ∀O:ordered_uniform_space.∀l,r:O.∀P:{[l,r]} square → Prop.∀OP:O square → Prop.Prop.
@@ -99,9 +99,6 @@ lemma bs_of_ss:
 notation < "x \sub \neq" with precedence 91 for @{'bsss $x}.
 interpretation "bs_of_ss" 'bsss x = (bs_of_ss _ _ _ x).
 
-alias symbol "square" (instance 7) = "ordered set square".
-alias symbol "square" (instance 13) = "ordered set square".
-alias symbol "dependent_pair" = "dependent set".
 lemma ss_of_bs: 
  ∀O:ordered_set.∀u,v:O.
   ∀b:O square.\fst b ∈ [u,v] → \snd b ∈ [u,v] → {[u,v]} square ≝ 
@@ -161,7 +158,7 @@ interpretation "Ordered uniform space segment" 'segment_set a b =
  (segment_ordered_uniform_space _ a b).
 
 (* Lemma 3.2 *)
-alias symbol "pi1" = "sigT \fst".
+alias symbol "pi1" = "exT \fst".
 lemma restric_uniform_convergence:
  ∀O:ordered_uniform_space.∀l,u:O.
   ∀x:{[l,u]}.

diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma
index 2e0e73bc6edc3c08f10767adc737d38d3150373e..241882bdd11fb5fff540b3832f5f7d09ad3daf03 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/property_sigma.ma
+++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma
@@ -63,7 +63,6 @@ lemma sigma_cauchy:
   ∀C:ordered_uniform_space.property_sigma C →
     ∀a:sequence C.∀l:C.(a ↑ l ∨ a ↓ l) → a is_cauchy → a uniform_converges l.
 intros 8; cases (H ? H3) (w H5); cases H5 (H8 H9); clear H5;
-alias symbol "pair" = "Pair construction".
 letin spec ≝ (λz,k:nat.∀i,j,l:nat.k ≤ i → k ≤ j → l ≤ z → w l 〈a i,a j〉);
 letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
   match i with

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index b4430d6edff7d4daaa16eaa9a899786a4dea2498..f0260471f73a1a944069a564db518445ab65f70d 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -238,7 +238,7 @@ interpretation "Ordered set sergment in" 'segment_in a b x= (segment _ a b x).
 
 lemma segment_ordered_set: 
   ∀O:ordered_set.∀u,v:O.ordered_set.
-intros (O u v); apply (mk_ordered_set (sigT ? (λx.x ∈ [u,v])));
+intros (O u v); apply (mk_ordered_set (∃x.x ∈ [u,v]));
 [1: intros (x y); apply (\fst x ≰ \fst y);
 |2: intro x; cases x; simplify; apply os_coreflexive;
 |3: intros 3 (x y z); cases x; cases y ; cases z; simplify; apply os_cotransitive]