---

Step * of Lemma adjacent-before

∀[T:Type]. ∀L:T List. ∀x,y:T.  (adjacent(T;L;x;y) ⇒ x before y ∈ L)
BY
{ (RepUR``adjacent l_before sublist`` 0 THEN Auto THEN ExRepD THEN Auto') }

1
1. [T] : Type
2. L : T List
3. x : T
4. y : T
5. i : ℕ||L|| - 1
6. x = L[i] ∈ T
7. y = L[i + 1] ∈ T
⊢ ∃f:ℕ2 ⟶ ℕ||L||. (increasing(f;2) ∧ (∀j:ℕ2. ([x; y][j] = L[f j] ∈ T)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}x,y:T.    (adjacent(T;L;x;y)  {}\mRightarrow{}  x  before  y  \mmember{}  L)


By

---

Latex:
(RepUR``adjacent  l\_before  sublist``  0  THEN  Auto  THEN  ExRepD  THEN  Auto')

---

Home Index