From f34fc116009aa590a6036afa4df24f1edeafd91d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 7 Nov 2008 14:31:25 +0000
Subject: [PATCH] some other simplification

---
 .../matita/contribs/dama/dama/ordered_uniform.ma  | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
index 36ba2d287..5d6559d1f 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
@@ -78,20 +78,17 @@ lemma restriction_agreement :
   ∀O:ordered_uniform_space.∀s:‡O.∀P:{[s]} squareO → Prop.∀OP:O squareO → Prop.Prop.
 apply(λO:ordered_uniform_space.λs:‡O.
        λP:{[s]} squareO → Prop. λOP:O squareO → Prop.
-          ∀b:O squareO.∀H1,H2.(P b → OP b) ∧ (OP b → P b));
-[5,7: apply H1|6,8:apply H2]skip;
+          ∀b:{[s]} squareO.(P b → OP b) ∧ (OP b → P b));
 qed.
 
 lemma unrestrict: ∀O:ordered_uniform_space.∀s:‡O.∀U,u.∀x:{[s]} squareO.
   restriction_agreement ? s U u → U x → u x.
-intros 6; cases x (b b1); cases b (w1 H1); cases b1 (w2 H2); clear b b1 x; 
-cases (H 〈w1,w2〉 H1 H2) (L _); intro Uw; apply L; apply Uw;
+intros 6; cases (H x); assumption;
 qed.
 
 lemma restrict: ∀O:ordered_uniform_space.∀s:‡O.∀U,u.∀x:{[s]} squareO.
   restriction_agreement ? s U u → u x → U x.
-intros 5; cases x (b b1); cases b (w1 H1); cases b1 (w2 H2); clear b1 b x;
-intros (Ra uw); cases (Ra 〈w1,w2〉 H1 H2) (_ R); apply R; apply uw;
+intros 6; cases (H x); assumption;
 qed.
 
 lemma invert_restriction_agreement: 
@@ -99,9 +96,9 @@ lemma invert_restriction_agreement:
    ∀U:{[s]} squareO → Prop.∀u:O squareO → Prop.
     restriction_agreement ? s U u →
     restriction_agreement ? s (\inv U) (\inv u).
-intros 8; split; intro;
-[1: apply (unrestrict ???? (segment_square_of_ordered_set_square ?? 〈\snd b,\fst b〉 H2 H1) H H3);
-|2: apply (restrict ???? (segment_square_of_ordered_set_square ?? 〈\snd b,\fst b〉 H2 H1) H H3);]
+intros 6; cases b;
+generalize in match (H 〈h1,h〉); cases h; cases h1; simplify; 
+intro X; cases X; split; assumption; 
 qed. 
 
 lemma bs2_of_bss2: 
-- 
2.39.2