From 99f153e43f18bc682339bed41c8230af2ac6fd2f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 12 Jun 2008 08:40:06 +0000 Subject: [PATCH] fixed some regressions --- helm/software/matita/contribs/dama/dama/lebesgue.ma | 4 ++-- .../matita/contribs/dama/dama/property_exhaustivity.ma | 5 +++-- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma index bab1e26fa..46fe6e422 100644 --- 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 cf3a5b057..44be29543 100644 --- 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;] -- 2.39.2