---

Step * 1 of Lemma before-adjacent


1. [T] : Type
2. x : T
3. y : T
4. no_repeats(T;[])
5. adjacent(T;[];x;y)
6. z : T
7. z before y ∈ []
⊢ z before x ∈ [] ∨ (z = x ∈ T)
BY
{ (FLemma `adjacent-nil` [5] THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  x  :  T
3.  y  :  T
4.  no\_repeats(T;[])
5.  adjacent(T;[];x;y)
6.  z  :  T
7.  z  before  y  \mmember{}  []
\mvdash{}  z  before  x  \mmember{}  []  \mvee{}  (z  =  x)


By

---

Latex:
(FLemma  `adjacent-nil`  [5]  THEN  Auto)

---

Home Index