From c33fae30b4ce40198b8e1889ea1c1b58697cd567 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 27 Oct 2008 20:53:43 +0000
Subject: [PATCH] WIP

---
 .../dama/dama/property_exhaustivity.ma        | 24 +++++++++++++++++--
 1 file changed, 22 insertions(+), 2 deletions(-)

diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
index fc7121349..0e0f013e9 100644
--- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
+++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
@@ -92,8 +92,28 @@ lemma restrict_uniform_convergence_uparrow:
      ∀a:sequence (segment_ordered_uniform_space C s).
       ∀x:C. ⌊n,\fst (a n)⌋ ↑ x → 
        in_segment (os_l C) s x ∧ ∀h:x ∈ s.a uniform_converges ≪x,h≫.
-intros; cases H2 (Ha Hx); clear H2; cases Hx; split;
-[1: apply prove_in_segment; 
+intros; split;
+[1: unfold in H2; cases H2; clear H2;unfold in H3 H4; cases H4; clear H4; unfold in H2;
+    cases (wloss_prop (os_l C)) (W W); apply prove_in_segment; unfold; rewrite <W;
+    simplify;
+    [ apply (le_transitive ?? x ? (H2 O));  
+      lapply (under_wloss_upperbound (os_r C) ?? (h_segment_upperbound (os_r C) s a) O) as K;
+      unfold in K; whd in K:(?%????); simplify in K; rewrite <W in K; apply K;
+    | intro; cases (H5 ? H4); clear H5 H4;    
+      lapply (under_wloss_upperbound (os_l C) ?? (segment_upperbound s a) w) as K;
+      unfold in K; whd in K:(?%????); simplify in K; rewrite <W in K;
+      apply K; apply H6;
+    | intro; unfold in H4; rewrite <W in H4;
+      lapply depth=0 (H5 (seg_u_ (os_l C) s)) as k; unfold in k:(%???→?);
+      simplify in k; rewrite <W in k; lapply (k
+     simplify;intro; cases (H5 ? H4); clear H5 H4;    
+      lapply (under_wloss_upperbound (os_l C) ?? (segment_upperbound s a) w) as K;
+      unfold in K; whd in K:(?%????); simplify in K; rewrite <W in K;
+      apply K; apply H6;    
+      
+      
+      
+    cases H2 (Ha Hx); clear H2; cases Hx; split; 
     lapply depth=0 (under_wloss_upperbound (os_l C) ?? (segment_upperbound s a) O) as W1;
     lapply depth=0 (under_wloss_upperbound (os_r C) ?? (h_segment_upperbound (os_r C) s a) O) as W2;
     lapply (H2 O); simplify in Hletin; simplify in W2 W1;
-- 
2.39.2