---

Step * of Lemma select_wf

∀[A:Type]. ∀[l:A List]. ∀[n:ℤ].  (l[n] ∈ A) supposing (n < ||l|| and (0 ≤ n))
BY
{ ((InductionOnList THEN Auto') THEN (RecUnfold `select` 0 THEN Reduce 0) THEN AutoSplit)⋅ }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[l:A  List].  \mforall{}[n:\mBbbZ{}].    (l[n]  \mmember{}  A)  supposing  (n  <  ||l||  and  (0  \mleq{}  n))


By

---

Latex:
((InductionOnList  THEN  Auto')  THEN  (RecUnfold  `select`  0  THEN  Reduce  0)  THEN  AutoSplit)\mcdot{}

---

Home Index