---

Step * 1 1 1 1 of Lemma before-adjacent2


1. [T] : Type
2. L : T List
3. x : T
4. y : T
5. ∀[x,y:T].  ¬(x = y ∈ T) supposing x before y ∈ L
6. adjacent(T;L;x;y)
7. z : T
8. x before z ∈ L
9. (x ∈ L)
10. (y ∈ L)
11. (z ∈ L)
12. z before y ∈ L
13. z = x ∈ T
14. ¬z before x ∈ L
⊢ y before z ∈ L ∨ (z = y ∈ T)
BY
{ ((Assert ¬(x = z ∈ T) BY Auto) THEN D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List
3.  x  :  T
4.  y  :  T
5.  \mforall{}[x,y:T].    \mneg{}(x  =  y)  supposing  x  before  y  \mmember{}  L
6.  adjacent(T;L;x;y)
7.  z  :  T
8.  x  before  z  \mmember{}  L
9.  (x  \mmember{}  L)
10.  (y  \mmember{}  L)
11.  (z  \mmember{}  L)
12.  z  before  y  \mmember{}  L
13.  z  =  x
14.  \mneg{}z  before  x  \mmember{}  L
\mvdash{}  y  before  z  \mmember{}  L  \mvee{}  (z  =  y)


By

---

Latex:
((Assert  \mneg{}(x  =  z)  BY  Auto)  THEN  D  -1  THEN  Auto)

---

Home Index