---

Step * 1 of Lemma word-rel-append2


1. X : Type
2. w1 : (X + X) List
3. x : (X + X) List
4. y : (X + X) List
5. x@0 : X + X
6. y@0 : X + X
7. a : (X + X) List
8. b : (X + X) List
9. x@0 = -y@0
10. x = (a @ [x@0; y@0] @ b) ∈ ((X + X) List)
11. y = (a @ b) ∈ ((X + X) List)
⊢ ∃a,b:(X + X) List
   (x@0 = -y@0 ∧ ((w1 @ x) = (a @ [x@0; y@0] @ b) ∈ ((X + X) List)) ∧ ((w1 @ y) = (a @ b) ∈ ((X + X) List)))
BY
{ (D 0 With ⌜w1 @ a⌝  THEN Auto THEN RWO "-3" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  w1  :  (X  +  X)  List
3.  x  :  (X  +  X)  List
4.  y  :  (X  +  X)  List
5.  x@0  :  X  +  X
6.  y@0  :  X  +  X
7.  a  :  (X  +  X)  List
8.  b  :  (X  +  X)  List
9.  x@0  =  -y@0
10.  x  =  (a  @  [x@0;  y@0]  @  b)
11.  y  =  (a  @  b)
\mvdash{}  \mexists{}a,b:(X  +  X)  List.  (x@0  =  -y@0  \mwedge{}  ((w1  @  x)  =  (a  @  [x@0;  y@0]  @  b))  \mwedge{}  ((w1  @  y)  =  (a  @  b)))


By

---

Latex:
(D  0  With  \mkleeneopen{}w1  @  a\mkleeneclose{}    THEN  Auto  THEN  RWO  "-3"  0  THEN  Auto)

---

Home Index