fixed some regressions

diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma
index bab1e26faef33c6bc09544c31b7895ae2fd1b8cf..46fe6e4223afa0136c19bed8423339b88308758c 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma
@@ -76,10 +76,10 @@ split;
     [1: intro j; cases (Hxy j); cases H3; cases H4; split;
         [apply (H5 0);|apply (H7 0)]
     |2: cases (H l u Xi X) (Ux Uy); apply Ux; cases Hx; split; [apply H3;]
-        cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y) Hy);
+        cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y));[2:apply Hy];
         exists [apply w] apply H7; 
     |3: cases (H l u Yi X) (Ux Uy); apply Uy; cases Hy; split; [apply H3;]
-        cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y) Hy);
+        cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y));[2:apply Hy];
         exists [apply w] apply H7;]]
 qed.
  

diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
index cf3a5b0574cfe099fd04f79cb29f62ef087cb416..44be295434eb62f3b72b9c391c396eb431126c83 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
+++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
@@ -37,7 +37,7 @@ lemma segment_preserves_uparrow:
     (λn.fst (a n)) ↑ x → a ↑ (sig_in ?? x h).
 intros; cases H (Ha Hx); split [apply Ha] cases Hx; 
 split; [apply H1] intros;
-cases (H2 (fst y) H3); exists [apply w] assumption;
+cases (H2 (fst y)); [2: apply H3;] exists [apply w] assumption;
 qed.
 
 lemma segment_preserves_downarrow:
@@ -45,7 +45,7 @@ lemma segment_preserves_downarrow:
     (λn.fst (a n)) ↓ x → a ↓ (sig_in ?? x h).
 intros; cases H (Ha Hx); split [apply Ha] cases Hx; 
 split; [apply H1] intros;
-cases (H2 (fst y) H3); exists [apply w] assumption;
+cases (H2 (fst y));[2:apply H3]; exists [apply w] assumption;
 qed.
     
 (* Fact 2.18 *)
@@ -54,6 +54,7 @@ lemma segment_cauchy:
     a is_cauchy → (λn:nat.fst (a n)) is_cauchy.
 intros 7; 
 alias symbol "pi1" (instance 3) = "pair pi1".
+alias symbol "pi2" = "pair pi2".
 apply (H (λx:{[l,u]} square.U 〈fst (fst x),fst (snd x)〉));
 (unfold segment_ordered_uniform_space; simplify);
 exists [apply U] split; [assumption;]