---

Step * 1 of Lemma adjacent-member


1. [T] : Type
2. L : T List@i
3. x : T@i
4. y : T@i
5. adjacent(T;L;x;y)@i
6. x before y ∈ L
7. (y ∈ L)
8. (x ∈ L)
⊢ {(x ∈ L) ∧ (y ∈ L)}
BY
{ (Unfold `guard` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List@i
3.  x  :  T@i
4.  y  :  T@i
5.  adjacent(T;L;x;y)@i
6.  x  before  y  \mmember{}  L
7.  (y  \mmember{}  L)
8.  (x  \mmember{}  L)
\mvdash{}  \{(x  \mmember{}  L)  \mwedge{}  (y  \mmember{}  L)\}


By

---

Latex:
(Unfold  `guard`  0  THEN  Auto)

---

Home Index