---

Step * of Lemma round-robin-list-index

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[L:T List].  (round-robin(L) outl(list-index(eq;L;x))) = x ∈ T supposing (x ∈ L)
BY
{ ((InstLemma `list-index-property` []⋅ THEN RepeatFor 5 (ParallelLast'))
   THEN RepUR ``round-robin`` 0
   THEN Auto
   THEN NthHypSq (-1)
   THEN RepeatFor 2 (EqCD)
   THEN Auto
   THEN BLemma `rem_base_case` 
   THEN Auto
   THEN (Assert ↑isl(list-index(eq;L;x)) BY
               (RWO "isl-list-index" 0 THEN Auto))
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[L:T  List].
    (round-robin(L)  outl(list-index(eq;L;x)))  =  x  supposing  (x  \mmember{}  L)


By

---

Latex:
((InstLemma  `list-index-property`  []\mcdot{}  THEN  RepeatFor  5  (ParallelLast'))
  THEN  RepUR  ``round-robin``  0
  THEN  Auto
  THEN  NthHypSq  (-1)
  THEN  RepeatFor  2  (EqCD)
  THEN  Auto
  THEN  BLemma  `rem\_base\_case` 
  THEN  Auto
  THEN  (Assert  \muparrow{}isl(list-index(eq;L;x))  BY
                          (RWO  "isl-list-index"  0  THEN  Auto))
  THEN  Auto)

---

Home Index