From 2de5506abeebb60e552d68b828d8c481ee7be742 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 31 Jan 2008 12:43:37 +0000
Subject: [PATCH] snapshot

---
 helm/software/matita/dama/TODO       |   2 +
 helm/software/matita/dama/excess.ma  |  85 +++++---
 helm/software/matita/dama/lattice.ma | 299 ++++++++++++++++++++++++++-
 3 files changed, 347 insertions(+), 39 deletions(-)

diff --git a/helm/software/matita/dama/TODO b/helm/software/matita/dama/TODO
index 6e2ccdd68..353329bea 100644
--- a/helm/software/matita/dama/TODO
+++ b/helm/software/matita/dama/TODO
@@ -1,2 +1,4 @@
 changing file resets the display-notation ref, but not the GUI tick
 mettere una maction in tutti i body (ma forse non basta)
+la visualizzazione dellea notazione se viene disttivata e poi se ne definisce una... la rende causa
+il fatto che disabilitarla significa rimuovere quelle definite fino ad ora, non disabilitarla in senso proprio.
diff --git a/helm/software/matita/dama/excess.ma b/helm/software/matita/dama/excess.ma
index 826ae8c0b..9068d297b 100644
--- a/helm/software/matita/dama/excess.ma
+++ b/helm/software/matita/dama/excess.ma
@@ -26,7 +26,32 @@ record excess_base : Type ≝ {
   exc_cotransitive: cotransitive ? exc_excess 
 }.
 
-interpretation "excess" 'nleq a b = (cic:/matita/excess/exc_excess.con _ a b). 
+interpretation "Excess base excess" 'nleq a b = (cic:/matita/excess/exc_excess.con _ a b). 
+
+(* E(#,≰) → E(#,sym(≰)) *)
+lemma make_dual_exc: excess_base → excess_base.
+intro E;
+apply (mk_excess_base (exc_carr E));
+  [ apply (λx,y:E.y≰x);|apply exc_coreflexive;
+  | unfold cotransitive; simplify; intros (x y z H);
+    cases (exc_cotransitive E ??z H);[right|left]assumption]
+qed.
+
+record excess_dual : Type ≝ {
+  exc_dual_base:> excess_base;
+  exc_dual_dual_ : excess_base;
+  exc_with: exc_dual_dual_ = make_dual_exc exc_dual_base
+}.
+
+lemma mk_excess_dual_smart: excess_base → excess_dual.
+intro; apply mk_excess_dual; [apply e| apply (make_dual_exc e)|reflexivity]
+qed.
+
+definition exc_dual_dual: excess_dual → excess_base.
+intro E; apply (make_dual_exc E);
+qed. 
+
+coercion cic:/matita/excess/exc_dual_dual.con.
 
 record apartness : Type ≝ {
   ap_carr:> Type;
@@ -50,32 +75,44 @@ intros (E); apply (mk_apartness E (λa,b:E. a ≰ b ∨ b ≰ a));
 qed.
 
 record excess_ : Type ≝ {
-  exc_exc:> excess_base;
+  exc_exc:> excess_dual;
   exc_ap_: apartness;
-  exc_with: ap_carr exc_ap_ = exc_carr exc_exc
+  exc_with1: ap_carr exc_ap_ = exc_carr exc_exc
 }.
 
 definition exc_ap: excess_ → apartness.
 intro E; apply (mk_apartness E); unfold Type_OF_excess_; 
-cases (exc_with E); simplify;
+cases (exc_with1 E); simplify;
 [apply (ap_apart (exc_ap_ E));
 |apply ap_coreflexive;|apply ap_symmetric;|apply ap_cotransitive] 
 qed.
 
 coercion cic:/matita/excess/exc_ap.con.
 
+interpretation "Excess excess_" 'nleq a b =
+ (cic:/matita/excess/exc_excess.con (cic:/matita/excess/excess_base_OF_excess_1.con _) a b).
+
 record excess : Type ≝ {
   excess_carr:> excess_;
   ap2exc: ∀y,x:excess_carr. y # x → y ≰ x ∨ x ≰ y;
   exc2ap: ∀y,x:excess_carr.y ≰ x ∨ x ≰ y →  y # x 
 }.
 
+interpretation "Excess excess" 'nleq a b =
+ (cic:/matita/excess/exc_excess.con (cic:/matita/excess/excess_base_OF_excess1.con _) a b).
+ 
+interpretation "Excess (dual) excess" 'ngeq a b =
+ (cic:/matita/excess/exc_excess.con (cic:/matita/excess/excess_base_OF_excess.con _) a b).
+
 definition strong_ext ≝ λA:apartness.λop:A→A.∀x,y. op x # op y → x # y.
 
-definition le ≝ λE:excess.λa,b:E. ¬ (a ≰ b).
+definition le ≝ λE:excess_base.λa,b:E. ¬ (a ≰ b).
 
-interpretation "ordered sets less or equal than" 'leq a b = 
- (cic:/matita/excess/le.con _ a b).
+interpretation "Excess less or equal than" 'leq a b = 
+ (cic:/matita/excess/le.con (cic:/matita/excess/excess_base_OF_excess1.con _) a b).
+
+interpretation "Excess less or equal than" 'geq a b = 
+ (cic:/matita/excess/le.con (cic:/matita/excess/excess_base_OF_excess.con _) a b).
 
 lemma le_reflexive: ∀E.reflexive ? (le E).
 unfold reflexive; intros 3 (E x H); apply (exc_coreflexive ?? H);
@@ -89,14 +126,15 @@ qed.
 definition eq ≝ λA:apartness.λa,b:A. ¬ (a # b).
 
 notation "hvbox(a break ≈ b)" non associative with precedence 50 for @{ 'napart $a $b}.    
-interpretation "alikeness" 'napart a b =
-  (cic:/matita/excess/eq.con _ a b). 
+interpretation "Apartness alikeness" 'napart a b = (cic:/matita/excess/eq.con _ a b). 
+interpretation "Excess alikeness" 'napart a b = (cic:/matita/excess/eq.con (cic:/matita/excess/excess_base_OF_excess1.con _) a b). 
+interpretation "Excess (dual) alikeness" 'napart a b = (cic:/matita/excess/eq.con (cic:/matita/excess/excess_base_OF_excess.con _) a b). 
 
-lemma eq_reflexive:∀E. reflexive ? (eq E).
+lemma eq_reflexive:∀E:apartness. reflexive ? (eq E).
 intros (E); unfold; intros (x); apply ap_coreflexive; 
 qed.
 
-lemma eq_sym_:∀E.symmetric ? (eq E).
+lemma eq_sym_:∀E:apartness.symmetric ? (eq E).
 unfold symmetric; intros 5 (E x y H H1); cases (H (ap_symmetric ??? H1)); 
 qed.
 
@@ -105,7 +143,7 @@ lemma eq_sym:∀E:apartness.∀x,y:E.x ≈ y → y ≈ x ≝ eq_sym_.
 (* SETOID REWRITE *)
 coercion cic:/matita/excess/eq_sym.con.
 
-lemma eq_trans_: ∀E.transitive ? (eq E).
+lemma eq_trans_: ∀E:apartness.transitive ? (eq E).
 (* bug. intros k deve fare whd quanto basta *)
 intros 6 (E x y z Exy Eyz); intro Axy; cases (ap_cotransitive ???y Axy); 
 [apply Exy|apply Eyz] assumption.
@@ -118,7 +156,8 @@ notation > "'Eq'≈" non associative with precedence 50 for @{'eqrewrite}.
 interpretation "eq_rew" 'eqrewrite = (cic:/matita/excess/eq_trans.con _ _ _).
 
 alias id "antisymmetric" = "cic:/matita/constructive_higher_order_relations/antisymmetric.con".
-lemma le_antisymmetric: ∀E.antisymmetric ? (le E) (eq ?).
+lemma le_antisymmetric: 
+  ∀E:excess.antisymmetric ? (le (excess_base_OF_excess1 E)) (eq E).
 intros 5 (E x y Lxy Lyx); intro H; 
 cases (ap2exc ??? H); [apply Lxy;|apply Lyx] assumption;
 qed.
@@ -136,8 +175,8 @@ lemma lt_transitive: ∀E.transitive ? (lt E).
 intros (E); unfold; intros (x y z H1 H2); cases H1 (Lxy Axy); cases H2 (Lyz Ayz); 
 split; [apply (le_transitive ???? Lxy Lyz)] clear H1 H2;
 elim (ap2exc ??? Axy) (H1 H1); elim (ap2exc ??? Ayz) (H2 H2); [1:cases (Lxy H1)|3:cases (Lyz H2)]
-clear Axy Ayz;lapply (exc_cotransitive E) as c; unfold cotransitive in c;
-lapply (exc_coreflexive E) as r; unfold coreflexive in r;
+clear Axy Ayz;lapply (exc_cotransitive (exc_dual_base E)) as c; unfold cotransitive in c;
+lapply (exc_coreflexive (exc_dual_base E)) as r; unfold coreflexive in r;
 [1: lapply (c ?? y H1) as H3; elim H3 (H4 H4); [cases (Lxy H4)|cases (r ? H4)]
 |2: lapply (c ?? x H2) as H3; elim H3 (H4 H4); [apply exc2ap; right; assumption|cases (Lxy H4)]]
 qed.
@@ -177,6 +216,7 @@ interpretation "ap_rewl" 'aprewritel = (cic:/matita/excess/ap_rewl.con _ _ _).
 notation > "'Ap'≫" non associative with precedence 50 for @{'aprewriter}.
 interpretation "ap_rewr" 'aprewriter = (cic:/matita/excess/ap_rewr.con _ _ _).
 
+alias symbol "napart" = "Apartness alikeness".
 lemma exc_rewl: ∀A:excess.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z.
 intros (A x z y Exy Ayz); elim (exc_cotransitive ???x Ayz); [2:assumption]
 cases Exy; apply exc2ap; right; assumption;
@@ -237,18 +277,3 @@ qed.
 definition total_order_property : ∀E:excess. Type ≝ 
   λE:excess. ∀a,b:E. a ≰ b → b < a.
 
-(* E(#,≰) → E(#,sym(≰)) *)
-lemma dual_exc: excess→ excess.
-intro E; apply mk_excess;
-[1: apply mk_excess_;
-  [1: apply (mk_excess_base (exc_carr (excess_carr E)));
-      [ apply (λx,y:E.y≰x);|apply exc_coreflexive;
-      | unfold cotransitive; simplify; intros (x y z H);
-        cases (exc_cotransitive E ??z H);[right|left]assumption]
-  |2: apply (exc_ap_ E);
-  |3: apply (exc_with E);]
-|2: simplify; intros (y x H); fold simplify (y#x) in H;
-    apply ap2exc; apply ap_symmetric; apply H;
-|3: simplify; intros; fold simplify (y#x); apply exc2ap; 
-    cases o; [right|left]assumption]
-qed.
diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index ef0213425..79bc27ee1 100644
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -30,8 +30,8 @@ lemma excess_of_semi_lattice_base: semi_lattice_base → excess.
 intro l;
 apply mk_excess;
 [1: apply mk_excess_;
-    [1: 
-    
+    [1: apply mk_excess_dual_smart;
+         
   apply (mk_excess_base (sl_carr l));
     [1: apply (λa,b:sl_carr l.a # (a ✗ b));
     |2: unfold; intros 2 (x H); simplify in H;
@@ -161,22 +161,303 @@ unfold excl; simplify;
 qed.
 *)
 
+(* ED(≰,≱) → EB(≰') → ED(≰',≱') *)
+lemma subst_excess_base: excess_dual → excess_base → excess_dual.
+intros; apply (mk_excess_dual_smart e1);
+qed.
+
+(* E_(ED(≰,≱),AP(#),c ED = c AP) → ED' → c DE' = c E_ → E_(ED',#,p) *)
+lemma subst_dual_excess: ∀e:excess_.∀e1:excess_dual.exc_carr e = exc_carr e1 → excess_.
+intros (e e1 p); apply (mk_excess_ e1 e); cases p; reflexivity;
+qed. 
+
+(* E(E_,H1,H2) → E_' → H1' → H2' → E(E_',H1',H2') *)
+alias symbol "nleq" = "Excess excess_".
+lemma subst_excess_: ∀e:excess. ∀e1:excess_. 
+  (∀y,x:e1. y # x → y ≰ x ∨ x ≰ y) →
+  (∀y,x:e1.y ≰ x ∨ x ≰ y →  y # x) →
+  excess.
+intros (e e1 H1 H2); apply (mk_excess e1 H1 H2); 
+qed. 
+
+(* SL(E,M,H2-5(#),H67(≰)) → E' → c E = c E' → H67'(≰') → SL(E,M,p2-5,H67') *)
+lemma subst_excess: 
+  ∀l:semi_lattice.
+  ∀e:excess. 
+  ∀p:exc_ap l = exc_ap e.
+  (∀x,y:e.(le (exc_dual_base e)) x y → x ≈ (?(sl_meet l)) x y) →
+  (∀x,y:e.(le (exc_dual_base e)) ((?(sl_meet l)) x y) y) → 
+  semi_lattice.
+[1,2:intro M;
+ change with ((λx.ap_carr x) e -> (λx.ap_carr x) e -> (λx.ap_carr x) e);
+ cases p; apply M;
+|intros (l e p H1 H2);
+ apply (mk_semi_lattice e);
+   [ change with ((λx.ap_carr x) e -> (λx.ap_carr x) e -> (λx.ap_carr x) e);
+     cases p; simplify; apply (sl_meet l);
+   |2: change in ⊢ (% → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_refl;
+   |3: change in ⊢ (% → % → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_comm;
+   |4: change in ⊢ (% → % → % → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_assoc;  
+   |5: change in ⊢ (% → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_strong_extm;
+   |6: clear H2; apply H1;
+   |7: clear H1; apply H2;]]
+qed.
+
+lemma excess_of_excess_base: excess_base → excess.
+intro eb;
+apply mk_excess;
+  [apply (mk_excess_ (mk_excess_dual_smart eb));
+    [apply (apartness_of_excess_base eb);
+    |reflexivity]
+  |2,3: intros; assumption]
+qed. 
+
+lemma subst_excess_base_in_semi_lattice: 
+  ∀sl:semi_lattice.
+  ∀eb:excess_base.
+  ∀p:exc_carr sl = exc_carr eb.
+  
+  mancano le 4 proprietà riscritte con p
+    
+  semi_lattice.
+intros (l eb H); apply (subst_excess l);
+  [apply (subst_excess_ l);
+    [apply (subst_dual_excess l);
+      [apply (subst_excess_base l eb);
+      |apply H;]
+    | change in \vdash (% -> % -> ?) with (exc_carr eb);
+    letin xxx \def (ap2exc l); clearbody xxx;
+    change in xxx:(%→%→?) with (Type_OF_semi_lattice l);
+    whd in ⊢ (?→?→? (? %) ? ?→?); 
+    unfold exc_ap;
+    simplify in ⊢ (?→?→%→?);
+
+intros 2;
+generalize in ⊢ (% -> ?); intro P;
+generalize in match x in ⊢ % as x;
+generalize in match y in ⊢ % as y; clear x y;
+
+    
+cases H; simplify;
+
+
+cut (Πy:exc_carr eb
+.Πx:exc_carr eb
+ .match 
+  (match H
+   in eq
+   return 
+  λright_1:Type
+  .(λmatched:eq Type (Type_OF_excess_ (excess__OF_semi_lattice l)) right_1
+    .eq Type (Type_OF_excess_ (excess__OF_semi_lattice l)) right_1)
+   with 
+  [refl_eq⇒refl_eq Type (Type_OF_excess_ (excess__OF_semi_lattice l))])
+   in eq
+   return 
+  λright_1:Type
+  .(λmatched:eq Type (ap_carr (exc_ap (excess__OF_semi_lattice l))) right_1
+    .right_1→right_1→Type)
+   with 
+  [refl_eq⇒ap_apart (exc_ap (excess__OF_semi_lattice l))] y x);[2:
+  
+
+    change in ⊢ (?→?→? % ? ?→?) with (exc_ap_ (excess__OF_semi_lattice l));
+    generalize in match H in \vdash (? -> %); cases H;  
+    cases H;
+    
+    
+normalize in ⊢ (?→?→?→? (? (? (? ? (% ? ?) ?)) ? ?) ?);
+whd in ⊢ (?→?→? % ? ?→?); change in ⊢ (?→?→? (? % ? ? ? ?) ? ?→?) with (exc_carr eb);
+cases H;
+      change in ⊢ (?→?→? % ? ?→?) with (exc_ap l);
+(subst_dual_excess (excess__OF_semi_lattice l)
+ (subst_excess_base (excess_dual_OF_semi_lattice l) eb) H)
+      
+      
+       unfold subst_excess_base;
+        unfold mk_excess_dual_smart;
+        unfold excess__OF_semi_lattice;
+        unfold excess_dual_OF_semi_lattice;
+        unfold excess_dual_OF_semi_lattice;
+        
+      reflexivity]
+*)
 
 record lattice_ : Type ≝ {
   latt_mcarr:> semi_lattice;
   latt_jcarr_: semi_lattice;
-  latt_with:  sl_exc latt_jcarr_ = dual_exc (sl_exc latt_mcarr)
+(*  latt_with1:   (subst_excess_
+                  (subst_dual_excess
+                    (subst_excess_base 
+                      (excess_dual_OF_excess (sl_exc latt_jcarr_))
+                      (excess_base_OF_excess (sl_exc latt_mcarr))))) =
+                sl_exc latt_jcarr_;   
+  
+*)  
+  latt_with1: excess_base_OF_excess1 (sl_exc latt_jcarr_) =  excess_base_OF_excess (sl_exc latt_mcarr);
+  latt_with2: excess_base_OF_excess (sl_exc latt_jcarr_) =  excess_base_OF_excess1 (sl_exc latt_mcarr);
+  latt_with3: apartness_OF_excess (sl_exc latt_jcarr_) = apartness_OF_excess (sl_exc latt_mcarr)
 }.
 
+axiom FALSE: False.
+
 lemma latt_jcarr : lattice_ → semi_lattice.
 intro l;
-apply (mk_semi_lattice (dual_exc l)); 
-unfold excess_OF_lattice_;
-cases (latt_with l); simplify;
-[apply sl_meet|apply sl_meet_refl|apply sl_meet_comm|apply sl_meet_assoc|
-apply sl_strong_extm| apply sl_le_to_eqm|apply sl_lem]
-qed. 
+apply mk_semi_lattice;
+  [apply mk_excess;
+    [apply mk_excess_;
+      [apply (mk_excess_dual_smart l);
+      |apply (exc_ap l);
+      |reflexivity]
+    |unfold mk_excess_dual_smart; simplify;
+     intros (x y H); cases (ap2exc ??? H); [right|left]  assumption;
+    |unfold mk_excess_dual_smart; simplify;
+     intros (x y H);cases H; apply exc2ap;[right|left] assumption;]] 
+unfold mk_excess_dual_smart; simplify;
+[1: change with ((λx.ap_carr x) l → (λx.ap_carr x) l → (λx.ap_carr x) l);
+    simplify; unfold apartness_OF_lattice_; 
+    cases (latt_with3 l); apply (sl_meet (latt_jcarr_ l)); 
+|2: change in ⊢ (%→?) with ((λx.ap_carr x) l); simplify;
+    unfold apartness_OF_lattice_;
+    cases (latt_with3 l); apply (sl_meet_refl (latt_jcarr_ l));
+|3: change in ⊢ (%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_;
+    cases (latt_with3 l); apply (sl_meet_comm (latt_jcarr_ l));
+|4: change in ⊢ (%→%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_;
+    cases (latt_with3 l); apply (sl_meet_assoc (latt_jcarr_ l));
+|5: change in ⊢ (%→%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_;
+    cases (latt_with3 l); apply (sl_strong_extm (latt_jcarr_ l));
+|7: 
+(*
+unfold excess_base_OF_lattice_; 
+    change in ⊢ (?→?→? ? (% ? ?) ?)
+    with (match latt_with3 l
+ in eq
+ return 
+λright_1:apartness
+.(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right_1
+  .ap_carr right_1→ap_carr right_1→ap_carr right_1)
+ with 
+[refl_eq⇒sl_meet (latt_jcarr_ l)]
+ : ?
+);
+  change in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?)
+  with ((λx.exc_carr x) (excess_base_OF_semi_lattice (latt_mcarr l)));
+  unfold excess_base_OF_lattice_ in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?);
+  simplify in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?);
+change in ⊢ (?→?→? ? (% ? ?) ?) with
+  (match refl_eq ? (excess__OF_semi_lattice (latt_mcarr l)) in eq
+   return (λR.λE:eq ? (excess_base_OF_semi_lattice (latt_mcarr l)) R.R → R → R)
+   with [refl_eq⇒ 
+     (match latt_with3 l in eq
+     return 
+       (λright:apartness
+        .(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right
+          .ap_carr right→ap_carr right→ap_carr right))
+     with [refl_eq⇒ sl_meet (latt_jcarr_ l)]
+     :
+     exc_carr (excess_base_OF_semi_lattice (latt_mcarr l))
+      →exc_carr (excess_base_OF_semi_lattice (latt_mcarr l))
+       →exc_carr (excess_base_OF_semi_lattice (latt_mcarr l))
+     )
+   ]);
+   generalize in ⊢ (?→?→? ? (match % return ? with [_⇒?] ? ?) ?);
+   unfold excess_base_OF_lattice_ in ⊢ (? ? ? %→?);
+   cases (latt_with1 l);
+  change in ⊢ (?→?→?→? ? (match ? return ? with [_⇒(?:%→%->%)] ? ?) ?)
+  with ((λx.ap_carr x) (latt_mcarr l));
+  simplify in ⊢ (?→?→?→? ? (match ? return ? with [_⇒(?:%→%->%)] ? ?) ?);
+  cases (latt_with3 l);
+   
+   change in ⊢ (? ? % ?→?) with ((λx.ap_carr x) l);
+   simplify in ⊢ (% → ?);
+   change in ⊢ (?→?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
+     with ((λx.ap_carr x) (apartness_OF_lattice_ l));
+   unfold apartness_OF_lattice_;  
+   cases (latt_with3 l); simplify;
+   change in ⊢ (? ? ? %→%→%→?) with ((λx.exc_carr x) l);
+   unfold excess_base_OF_lattice_;
+   cases (latt_with1 l); simplify;
+   change in \vdash (? -> % -> % -> ?) with (exc_carr (excess_base_OF_semi_lattice (latt_jcarr_ l)));
+   change in ⊢ ((? ? % ?)→%→%→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
+     with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)));
+   simplify;
+   intro H;
+   unfold excess_base_OF_semi_lattice1;
+   unfold excess_base_OF_excess1;
+   unfold excess_base_OF_excess_1;
+   change 
+*)
+
+change in ⊢ (?→?→? ? (% ? ?) ?) with
+  (match refl_eq ? (Type_OF_lattice_ l) in eq
+   return (λR.λE:eq ? (Type_OF_lattice_ l) R.R → R → R)
+   with [refl_eq⇒ 
+     match latt_with3 l in eq
+     return 
+       (λright:apartness
+        .(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right
+          .ap_carr right→ap_carr right→ap_carr right))
+     with [refl_eq⇒ sl_meet (latt_jcarr_ l)]
+   ]);
+   generalize in ⊢ (?→?→? ? (match % return ? with [_⇒?] ? ?) ?);
+   change in ⊢ (? ? % ?→?) with ((λx.ap_carr x) l);
+   simplify in ⊢ (% → ?);
+   change in ⊢ (?→?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
+     with ((λx.ap_carr x) (apartness_OF_lattice_ l));
+   unfold apartness_OF_lattice_;  
+   cases (latt_with3 l); simplify;
+   change in ⊢ (? ? ? %→%→%→?) with ((λx.exc_carr x) l);
+   unfold excess_base_OF_lattice_;
+   cases (latt_with1 l); simplify;
+   change in \vdash (? -> % -> % -> ?) with (exc_carr (excess_base_OF_semi_lattice (latt_jcarr_ l)));
+   change in ⊢ ((? ? % ?)→%→%→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
+     with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)));
+   simplify;
+   intro H;
+   change in ⊢ (?→?→%) with (le (mk_excess_base 
+          ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
+          ((λx.exc_excess x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
+          ((λx.exc_coreflexive x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
+          ((λx.exc_cotransitive x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)))
+        ) (match H
+ in eq
+ return 
+λR:Type
+.(λE:eq Type (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) R
+  .R→R→R)
+ with 
+[refl_eq⇒sl_meet (latt_jcarr_ l)] x y) y); 
+ simplify in ⊢ (?→?→? (? % ???) ? ?); 
+ change in ⊢ (?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?)
+ with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l)));
+ simplify in  ⊢ (?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?);
+ lapply (match H in eq return 
+        λright.λe:eq ? (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) right.
+       
+∀x:right
+.∀y:right
+ .le
+  (mk_excess_base right ???)
+  (match e
+    in eq
+    return 
+   λR:Type.(λE:eq Type (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) R.R→R→R)
+    with 
+   [refl_eq⇒sl_meet (latt_jcarr_ l)] x y) y
+        with [refl_eq ⇒ ?]) as XX;
+  [cases e; apply (exc_excess (latt_jcarr_ l)); 
+  |unfold;cases e;simplify;apply (exc_coreflexive (latt_jcarr_ l)); 
+  |unfold;cases e;simplify;apply (exc_cotransitive (latt_jcarr_ l)); 
+  ||apply XX|
+  |apply XX;
+        
+         simplify; apply (sl_lem);
+|elim FALSE]
+qed.
+
+   
  
+    
 coercion cic:/matita/lattice/latt_jcarr.con.
 
 interpretation "Lattice meet" 'and a b =
-- 
2.39.2