---

Step * of Lemma l_tricotomy

∀[T:Type]. ∀x,y:T. ∀L:T List.  ((x ∈ L) ⇒ (y ∈ L) ⇒ (((x = y ∈ T) ∨ x before y ∈ L) ∨ y before x ∈ L))
BY
{ ((Unfolds ``l_member l_before`` 0 THEN Auto) THEN ExRepD) }

1
1. [T] : Type
2. x : T
3. y : T
4. L : T List
5. i1 : ℕ
6. i1 < ||L||
7. x = L[i1] ∈ T
8. i : ℕ
9. i < ||L||
10. y = L[i] ∈ T
⊢ ((x = y ∈ T) ∨ [x; y] ⊆ L) ∨ [y; x] ⊆ L

---

Latex:

---

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


By

---

Latex:
((Unfolds  ``l\_member  l\_before``  0  THEN  Auto)  THEN  ExRepD)

---

Home Index