From 5b584922369c076f9925a1598a7a9fe65708a44f Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 21 Jul 2010 15:34:49 +0000
Subject: [PATCH] ...

---
 .../software/matita/nlibrary/re/re-setoids.ma | 312 ++++++++++++++----
 1 file changed, 245 insertions(+), 67 deletions(-)

diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma
index a47d6defa..0b4c3365a 100644
--- a/helm/software/matita/nlibrary/re/re-setoids.ma
+++ b/helm/software/matita/nlibrary/re/re-setoids.ma
@@ -14,7 +14,7 @@
 
 include "datatypes/pairs.ma".
 include "datatypes/bool.ma".
-include "logic/cprop.ma".
+include "sets/sets.ma".
 
 ninductive Admit : CProp[0] ≝ .
 naxiom admit : Admit.
@@ -33,11 +33,11 @@ ndefinition LIST : setoid → setoid.
 #S; @(list S); @(eq_list S); ncases admit; nqed.  
 
 unification hint 0 ≔ S : setoid;
-  T ≟ carr S,
-  P1 ≟ refl ? (eq (LIST S)),
-  P2 ≟ sym ? (eq (LIST S)),
-  P3 ≟ trans ? (eq (LIST S)),
-  X ≟ mk_setoid (list S) (mk_equivalence_relation ? (eq_list S) P1 P2 P3)
+  P1 ≟ refl ? (eq0 (LIST S)),
+  P2 ≟ sym ? (eq0 (LIST S)),
+  P3 ≟ trans ? (eq0 (LIST S)),
+  X ≟ mk_setoid (list S) (mk_equivalence_relation ? (eq_list S) P1 P2 P3),
+  T ≟ carr S
 (*-----------------------------------------------------------------------*) ⊢
      carr X ≡ list T.
 
@@ -71,13 +71,16 @@ ndefinition associative ≝ λA:setoid.λf:A → A → A.∀x,y,z.f x (f y z) =
 ninductive one : Type[0] ≝ unit : one.
 
 ndefinition force ≝ 
-  λS:Type[1].λs:S.λT:Type[1].λt:T.λlock:one.
-    match lock return λ_.Type[1] with [ unit ⇒ T].
+  λS:Type[2].λs:S.λT:Type[2].λt:T.λlock:one.
+    match lock return λ_.Type[2] with [ unit ⇒ T].
 
-nlet rec lift (S:Type[1]) (s:S) (T:Type[1]) (t:T) (lock:one) on lock : force S s T t lock ≝ 
+nlet rec lift (S:Type[2]) (s:S) (T:Type[2]) (t:T) (lock:one) on lock : force S s T t lock ≝ 
  match lock return λlock.force S s T t lock with [ unit ⇒ t ].
 
-ncoercion lift : ∀S:Type[1].∀s:S.∀T:Type[1].∀t:T.∀lock:one. force S s T t lock ≝ lift
+ncoercion lift1 : ∀S:Type[1].∀s:S.∀T:Type[1].∀t:T.∀lock:one. force S s T t lock ≝ lift
+ on s : ? to force ?????.
+
+ncoercion lift2 : ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one. force S s T t lock ≝ lift
  on s : ? to force ?????.
 
 unification hint 0 ≔ R : setoid; 
@@ -85,27 +88,58 @@ unification hint 0 ≔ R : setoid;
 (* ---------------------------------------- *) ⊢ 
    setoid ≡ force ?(*Type[0]*) MR TR R lock.
 
+unification hint 0 ≔ R : setoid1; 
+   TR ≟ setoid1, MR ≟ (carr1 R), lock ≟ unit 
+(* ---------------------------------------- *) ⊢ 
+   setoid1 ≡ force ? MR TR R lock.
+
 ntheorem associative_append: ∀A:setoid.associative (list A) (append A).
 #A;#x;#y;#z;nelim x[//|#a;#x1;#H;nnormalize;/2/]nqed.
 
 interpretation "iff" 'iff a b = (iff a b).  
 
-naxiom eq_bool : bool → bool → CProp[0].
+ninductive eq (A:Type[0]) (x:A) : A → CProp[0] ≝ refl: eq A x x.
+
+nlemma eq_rect_Type0_r':
+ ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p.
+ #A; #a; #x; #p; ncases p; #P; #H; nassumption.
+nqed.
+
+nlemma eq_rect_Type0_r:
+ ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A; #a; #P; #p; #x0; #p0; napply (eq_rect_Type0_r' ??? p0); nassumption.
+nqed.
+
+nlemma eq_rect_CProp0_r':
+ ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p.
+ #A; #a; #x; #p; ncases p; #P; #H; nassumption.
+nqed.
+
+nlemma eq_rect_CProp0_r:
+ ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
+nqed.
+
+notation < "a = b" non associative with precedence 45 for @{ 'eqpp $a $b}.
+interpretation "bool eq" 'eqpp a b = (eq bool a b). 
+
 ndefinition BOOL : setoid.
-@bool; @eq_bool; ncases admit.nqed.
+@bool; @(eq bool); ncases admit.nqed.
 
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
+alias id "refl" = "cic:/matita/ng/properties/relations/refl.fix(0,1,3)".
 unification hint 0 ≔ ;
-  P1 ≟ refl ? (eq BOOL),
-  P2 ≟ sym ? (eq BOOL),
-  P3 ≟ trans ? (eq BOOL),
-  X ≟ mk_setoid bool (mk_equivalence_relation ? eq_bool P1 P2 P3)
+  P1 ≟ refl ? (eq0 BOOL),
+  P2 ≟ sym ? (eq0 BOOL),
+  P3 ≟ trans ? (eq0 BOOL),
+  X ≟ mk_setoid bool (mk_equivalence_relation ? (eq bool) P1 P2 P3)
 (*-----------------------------------------------------------------------*) ⊢
      carr X ≡ bool.
 
 nrecord Alpha : Type[1] ≝ { 
    acarr :> setoid;
-   eqb: acarr → acarr → bool (*; 
-   eqb_true: ∀x,y. (eqb x y = true) = (x = y)*)
+   eqb: acarr → acarr → bool; 
+   eqb_true: ∀x,y. (eqb x y = true) = (x = y)
 }.
  
 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
@@ -126,11 +160,11 @@ ndefinition RE : Alpha → setoid.
 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
 alias id "carr" = "cic:/matita/ng/sets/setoids/carr.fix(0,0,1)".
 unification hint 0 ≔ A : Alpha;
-  T ≟ acarr A,
-  P1 ≟ refl ? (eq (RE A)),
-  P2 ≟ sym ? (eq (RE A)),
-  P3 ≟ trans ? (eq (RE A)),
-  X ≟ mk_setoid (re T) (mk_equivalence_relation ? (eq_re A) P1 P2 P3)
+  P1 ≟ refl ? (eq0 (RE A)),
+  P2 ≟ sym ? (eq0 (RE A)),
+  P3 ≟ trans ? (eq0 (RE A)),
+  X ≟ mk_setoid (re A) (mk_equivalence_relation ? (eq_re A) P1 P2 P3),
+  T ≟ acarr A
 (*-----------------------------------------------------------------------*) ⊢
      carr X ≡ (re T).
 
@@ -152,49 +186,52 @@ interpretation "atom" 'ps a = (s ? a).
 notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
 interpretation "epsilon" 'epsilon = (e ?).
 
-notation "∅" non associative with precedence 90 for @{ 'empty }.
+notation "0" non associative with precedence 90 for @{ 'empty }.
 interpretation "empty" 'empty = (z ?).
 
-nrecord Setl (A : Type[0]) : Type[1] ≝ { in_set : A → CProp[0] }. 
-ndefinition Lang ≝ λA.Setl (list A).
-
-interpretation "in Setl" 'mem x l = (in_set ? l x).
-interpretation "compr Lang" 'comprehension t f = (mk_Setl t f).
+notation > "'lang' S" non associative with precedence 90 for @{ Ω^(list $S) }.
+notation > "'Elang' S" non associative with precedence 90 for @{ 𝛀^(list $S) }.
 
 nlet rec flatten S (l : list (list S)) on l : list S ≝ 
 match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
 
-nlet rec conjunct S (l : list (list S)) (L : Lang S) on l: CProp[0] ≝
+nlet rec conjunct S (l : list (list S)) (L : lang S) on l: CProp[0] ≝
 match l with [ nil ⇒ True | cons w tl ⇒ w ∈ L ∧ conjunct ? tl L ].
 
-ndefinition empty_lang ≝ λS.{ w ∈ list S | False }.
+
+ndefinition empty_set : ∀A.Ω^A ≝ λA.{ w | False }.
+notation "∅" non associative with precedence 90 for @{'emptyset}.
+interpretation "empty set" 'emptyset = (empty_set ?).
+
+(*
 notation "{}" non associative with precedence 90 for @{'empty_lang}.
 interpretation "empty lang" 'empty_lang = (empty_lang ?).
+*)
 
-ndefinition sing_lang ≝ λS:Alpha.λx.{ w ∈ list S | x = w }.
+ndefinition sing_lang : ∀A:setoid.∀x:A.Ω^A ≝ λS.λx.{ w | x = w }.
 interpretation "sing lang" 'singl x = (sing_lang ? x).
 
-ndefinition union ≝ λS.λl1,l2.{ w ∈ list S | w ∈ l1 ∨ w ∈ l2}.
-interpretation "union lang" 'union a b = (union ? a b).
+interpretation "subset construction with type" 'comprehension t \eta.x = 
+  (mk_powerclass t x).
 
-ndefinition cat ≝ 
-  λS:Alpha.λl1,l2.{ w ∈ list S | ∃w1,w2.w1 @ w2 = w ∧ w1 ∈ l1 ∧ w2 ∈ l2}.
+ndefinition cat : ∀A:setoid.∀l1,l2:lang A.lang A ≝ 
+  λS.λl1,l2.{ w ∈ list S | ∃w1,w2.w =_0 w1 @ w2 ∧ w1 ∈ l1 ∧ w2 ∈ l2}.
 interpretation "cat lang" 'pc a b = (cat ? a b).
 
-ndefinition star ≝ 
-  λS:Alpha.λl.{ w ∈ list S | ∃lw.flatten ? lw = w ∧ conjunct ? lw l}. 
+ndefinition star : ∀A:setoid.∀l:lang A.lang A ≝ 
+  λS.λl.{ w ∈ list S | ∃lw.flatten ? lw = w ∧ conjunct ? lw l}. 
 interpretation "star lang" 'pk l = (star ? l).
 
-notation > "𝐋 term 90 E" non associative with precedence 75 for @{L_re ? $E}.
-nlet rec L_re (S : Alpha) (r : re S) on r : Lang S ≝ 
+notation > "𝐋 term 70 E" non associative with precedence 75 for @{L_re ? $E}.
+nlet rec L_re (S : Alpha) (r : re S) on r : lang S ≝ 
 match r with
-[ z ⇒ {}
+[ z ⇒ ∅
 | e ⇒ { [ ] }
 | s x ⇒ { [x] }
 | c r1 r2 ⇒ 𝐋 r1 · 𝐋 r2
 | o r1 r2 ⇒  𝐋 r1 ∪ 𝐋 r2
 | k r1 ⇒ (𝐋 r1) ^*].
-notation "𝐋 term 90 E" non associative with precedence 75 for @{'L_re $E}.
+notation "𝐋 term 70 E" non associative with precedence 75 for @{'L_re $E}.
 interpretation "in_l" 'L_re E = (L_re ? E).
 
 notation "a || b" left associative with precedence 30 for @{'orb $a $b}.
@@ -232,53 +269,194 @@ interpretation "pempty" 'empty = (pz ?).
 notation > "|term 19 e|" non associative with precedence 70 for @{forget ? $e}.
 nlet rec forget (S: Alpha) (l : pitem S) on l: re S ≝
  match l with
-  [ pz ⇒ ∅
+  [ pz ⇒ 0
   | pe ⇒ ϵ
   | ps x ⇒ `x
   | pp x ⇒ `x
   | pc E1 E2 ⇒ (|E1| · |E2|)
   | po E1 E2 ⇒ (|E1| + |E2|)
   | pk E ⇒ |E|^* ].
-notation < ".|term 19 e|" non associative with precedence 70 for @{'forget $e}.
+notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.
 interpretation "forget" 'forget a = (forget ? a).
 
-notation > "𝐋\p\ term 90 E" non associative with precedence 90 for @{in_pl ? $E}.
-nlet rec in_pl (S : Alpha) (r : pitem S) on r : word S → Prop ≝ 
+notation > "𝐋\p\ term 70 E" non associative with precedence 75 for @{L_pi ? $E}.
+nlet rec L_pi (S : Alpha) (r : pitem S) on r : lang S ≝ 
 match r with
-[ pz ⇒ {}
-| pe ⇒ {}
-| ps _ ⇒ {}
+[ pz ⇒ ∅
+| pe ⇒ ∅
+| ps _ ⇒ ∅
 | pp x ⇒ { [x] }
-| pc r1 r2 ⇒ 𝐋\p\ r1 · 𝐋 .|r2| ∪ 𝐋\p\ r2
+| pc r1 r2 ⇒ 𝐋\p\ r1 · 𝐋 |r2| ∪ 𝐋\p\ r2
 | po r1 r2 ⇒ 𝐋\p\ r1 ∪ 𝐋\p\ r2
-| pk r1 ⇒ 𝐋\p\ r1 · 𝐋 (.|r1|^* ) ].
-notation > "𝐋\p term 90 E" non associative with precedence 90 for @{'in_pl $E}.
-notation "𝐋\sub(\p) term 90 E" non associative with precedence 90 for @{'in_pl $E}.
-interpretation "in_pl" 'in_pl E = (in_pl ? E).
-interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
+| pk r1 ⇒ 𝐋\p\ r1 · 𝐋 (|r1|^* ) ].
+notation > "𝐋\p term 70 E" non associative with precedence 75 for @{'L_pi $E}.
+notation "𝐋\sub(\p) term 70 E" non associative with precedence 75 for @{'L_pi $E}.
+interpretation "in_pl" 'L_pi E = (L_pi ? E).
+
+unification hint 0 ≔ S,a,b;
+   R ≟ LIST S
+(* -------------------------------------------- *) ⊢
+   eq_list S a b ≡ eq_rel (list S) (eq0 R) a b.
+
+notation > "B ⇒_0 C" right associative with precedence 72 for @{'umorph0 $B $C}.
+notation > "B ⇒_1 C" right associative with precedence 72 for @{'umorph1 $B $C}.
+notation "B ⇒\sub 0 C" right associative with precedence 72 for @{'umorph0 $B $C}.
+notation "B ⇒\sub 1 C" right associative with precedence 72 for @{'umorph1 $B $C}.
+
+interpretation "unary morphism 0" 'umorph0 A B = (unary_morphism A B).
+interpretation "unary morphism 1" 'umorph1 A B = (unary_morphism1 A B).
+
+ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid on _s: setoid to setoid1.
+
+nlemma exists_is_morph: (* BUG *) ∀S,T:setoid.∀P: S ⇒_1 (T ⇒_1 (CProp[0]:?)).
+  ∀y,z:S.y =_0 z → (Ex T (P y)) = (Ex T (P z)).
+#S T P y z E; @;
+##[ *; #x Px; @x; alias symbol "refl" (instance 4) = "refl".
+    alias symbol "prop2" (instance 2) = "prop21".
+    napply (. E^-1‡#); napply Px;
+##| *; #x Px; @x; napply (. E‡#); napply Px;##]
+nqed.
 
-ndefinition epsilon ≝ λS,b.if b then { ([ ] : word S) } else {}.
+ndefinition ex_morph : ∀S:setoid. (S ⇒_1 CPROP) ⇒_1 CPROP.
+#S; @; ##[ #P; napply (Ex ? P); ##| #P1 P2 E; @; 
+*; #x; #H; @ x; nlapply (E x x ?); //; *; /2/;
+nqed.
+ 
+nlemma d : ∀S:Alpha.
+ ∀ee: (setoid1_of_setoid (list S)) ⇒_1 (setoid1_of_setoid (list S)) ⇒_1 CPROP.
+ ∀x,y:list S.x = y →
+ let form ≝ comp1_unary_morphisms ??? (ex_morph (list S)) ee in
+  form x = form y.
+ #S ee x y E;
+ nletin F ≝ (comp1_unary_morphisms ??? (ex_morph (list S)) ee);
+ 
+ nnormalize;
+ nlapply (exists_is_morph (list S) (list S) ? ?? E);
+ 
+ nchange with (F x = F y);
+ nchange in E with (eq_rel1 ? (eq1 (setoid1_of_setoid (LIST S))) x y);
+ napply (.= † E);
+ napply #.
+nqed.
+
+
+E : w = w2
+  
+  
+  Σ(λx.(#‡E)‡#) : ∃x.x = w ∧ m → ∃x.x = w2 ∧ m 
+  λx.(#‡E)‡#    : ∀x.x = w ∧ m → x = w2 ∧ m 
+
+
+w;
+F ≟ ex_moprh ∘ G
+g ≟ fun11 G
+------------------------------
+ex (λx.g w x) ==?== fun11 F w
+
+x ⊢ fun11 ?h ≟ λw. ?g w x
+?G ≟ morphism_leibniz (T → S) ∘ ?h 
+------------------------------
+(λw. (λx:T.?g w x)) ==?== fun11 ?G
+
+...
+x ⊢ fun11 ?h ==?== λw. eq x w ∧ m [w] 
+(λw,x.eq x w ∧ m[w]) ==?== fun11 ?G
+ex (λx.?g w x) ==?== ex (λx.x = w ∧ m[w])
+
+ndefinition ex_morph : ∀S:setoid. (S ⇒_1 CPROP) ⇒_1 CPROP.
+#S; @; ##[ #P; napply (Ex ? P); ##| ncases admit. ##] nqed.
+
+ndefinition ex_morph1 : ∀S:setoid. (S ⇒_1 CPROP) ⇒_1 CPROP.
+#S; @; ##[ #P; napply (Ex ? (λx.P); ##| ncases admit. ##] nqed.
+
+
+nlemma d : ∀S:Alpha.
+ ∀ee: (setoid1_of_setoid (list S)) ⇒_1 (setoid1_of_setoid (list S)) ⇒_1 CPROP.
+ ∀x,y:list S.x = y →
+ let form ≝ comp1_unary_morphisms ??? (ex_morph (list S)) ee in
+  form x = form y.
+ #S ee x y E;
+ nletin F ≝ (comp1_unary_morphisms ??? (ex_morph (list S)) ee);
+ 
+ nnormalize;
+ 
+ nchange with (F x = F y);
+ nchange in E with (eq_rel1 ? (eq1 (setoid1_of_setoid (LIST S))) x y);
+ napply (.= † E);
+ napply #.
+nqed.
+
+
+nlemma d : ∀S:Alpha.∀ee: (setoid1_of_setoid (list S)) ⇒_1 (setoid1_of_setoid (list S)) ⇒_1 CPROP.∀x,y:list S.x = y →
+ let form ≝ comp1_unary_morphisms ??? (ex_morph (list S)) ee in
+  form x = form y.
+ #S ee x y E;
+ nletin F ≝ (comp1_unary_morphisms ??? (ex_morph (list S)) ee);
+ 
+ nnormalize;
+ 
+ nchange with (F x = F y);
+ nchange in E with (eq_rel1 ? (eq1 (setoid1_of_setoid (LIST S))) x y);
+ napply (.= † E);
+ napply #.
+nqed.
+ 
+  
+nlemma d : ∀S:Alpha.(setoid1_of_setoid (list S)) ⇒_1 CPROP.
+ #S; napply (comp1_unary_morphisms ??? (ex_morph (list S)) ?);
+ napply (eq1).
+  
+  
+  
+(*
+ndefinition comp_ex : ∀X,S,T,K.∀P:X ⇒_1 (S ⇒_1 T).∀Pc : (S ⇒_1 T) ⇒_1 K. X ⇒_1 K.
+ *)
+
+ndefinition L_pi_ext : ∀S:Alpha.∀r:pitem S.Elang S.
+#S r; @(𝐋\p r); #w1 w2 E; nelim r; /2/;
+##[ #x; @; #H; ##[ nchange in H ⊢ % with ([?]=?); napply ((.= H) E)]
+    nchange in H ⊢ % with ([?]=?); napply ((.= H) E^-1);
+##| #e1 e2 H1 H2; 
+    nchange in match (w1 ∈ 𝐋\p (?·?)) with ((∃_.?)∨?);
+    napply (.= (#‡H2));
+    napply (.= (Eexists ?? ? w1 w2 E)‡#);
+    
+    
+    nchange in match (w2 ∈ 𝐋\p (?·?)) with (?∨?);
+    napply (.= 
+    
+
+ //; napply (trans ?? ??? H E);
+   napply (trans (list S) (eq0 (LIST S)) ? [?] ?(*w1 [x] w2*) H E); 
+  nlapply (trans (list S) (eq0 (LIST S))).
+
+napply (.= H); nnormalize; nlapply (trans ? [x] w1 w2 E H); napply (.= ?) [napply (w1 = [x])] ##[##2: napply #; napply sym1; napply refl1 ]
+
+ndefinition epsilon ≝ 
+  λS:Alpha.λb.match b return λ_.lang S with [ true ⇒ { [ ] } | _ ⇒ ∅ ].
 
 interpretation "epsilon" 'epsilon = (epsilon ?).
 notation < "ϵ b" non associative with precedence 90 for @{'app_epsilon $b}.
 interpretation "epsilon lang" 'app_epsilon b = (epsilon ? b).
 
-ndefinition in_prl ≝ λS : Alpha.λp:pre S.  𝐋\p\ (\fst p) ∪ ϵ (\snd p).
+ndefinition L_pr ≝ λS : Alpha.λp:pre S.  𝐋\p\ (\fst p) ∪ ϵ (\snd p).
   
-interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
-interpretation "in_prl" 'in_pl E = (in_prl ? E).
+interpretation "L_pr" 'L_pi E = (L_pr ? E).
 
-nlemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = [ ] → w1 = [ ].
-#S w1; nelim w1; //. #x tl IH w2; nnormalize; #abs; ndestruct; nqed.
+nlemma append_eq_nil : ∀S:setoid.∀w1,w2:list S. w1 @ w2 = [ ] → w1 = [ ].
+#S w1; ncases w1; //. nqed.
 
 (* lemma 12 *)
-nlemma epsilon_in_true : ∀S.∀e:pre S. [ ] ∈ e ↔ \snd e = true.
+nlemma epsilon_in_true : ∀S:Alpha.∀e:pre S. [ ] ∈ 𝐋\p e = (\snd e = true).
 #S r; ncases r; #e b; @; ##[##2: #H; nrewrite > H; @2; /2/; ##] ncases b;//; 
-nnormalize; *; ##[##2:*] nelim e;
-##[ ##1,2: *; ##| #c; *; ##| #c; nnormalize; #; ndestruct; ##| ##7: #p H;
-##| #r1 r2 H G; *; ##[##2: /3/ by or_intror]
-##| #r1 r2 H1 H2; *; /3/ by or_intror, or_introl; ##]
-*; #w1; *; #w2; *; *; #defw1; nrewrite > (append_eq_nil … w1 w2 …); /3/ by {};//;
+*; ##[##2:*] nelim e;
+##[ ##1,2: *; ##| #c; *; ##| #c; *| ##7: #p H;
+##| #r1 r2 H G; *; ##[##2: nassumption; ##]
+##| #r1 r2 H1 H2; *; /2/ by {}]
+*; #w1; *; #w2; *; *; 
+##[ #defw1 H1 foo; napply H; napply (. #‡#); (append_eq_nil … defw1)^-1‡#);
+
+ nrewrite > (append_eq_nil ? … w1 w2 …); /3/ by {};//;
 nqed.
 
 nlemma not_epsilon_lp : ∀S.∀e:pitem S. ¬ (𝐋\p e [ ]).
-- 
2.39.2