---

Step * 1 of Lemma l_before_l_index


1. [T] : Type
2. dT : EqDecider(T)
3. L : T List
4. x : T
5. y : T
6. (x ∈ L)
7. (y ∈ L)
8. index(L;x) < index(L;y)
⊢ x before y ∈ L
BY
{ (((InstLemma `l_before_select` [⌜T⌝; ⌜L⌝; ⌜index(L;y)⌝; ⌜index(L;x)⌝])⋅ THENA Auto)
   THEN (NthHypEq (-1))
   THEN EqCD
   THEN Auto
   THEN RWO "select_l_index" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  dT  :  EqDecider(T)
3.  L  :  T  List
4.  x  :  T
5.  y  :  T
6.  (x  \mmember{}  L)
7.  (y  \mmember{}  L)
8.  index(L;x)  <  index(L;y)
\mvdash{}  x  before  y  \mmember{}  L


By

---

Latex:
(((InstLemma  `l\_before\_select`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}L\mkleeneclose{};  \mkleeneopen{}index(L;y)\mkleeneclose{};  \mkleeneopen{}index(L;x)\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  (NthHypEq  (-1))
  THEN  EqCD
  THEN  Auto
  THEN  RWO  "select\_l\_index"  0
  THEN  Auto)

---

Home Index