---

Step * of Lemma reverse_select_wf

∀[T:Type]. ∀[l:T List]. ∀[n:ℕ].  reverse_select(l;n) ∈ T supposing n < ||l||
BY
{ (Unfold `reverse_select` 0 THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[l:T  List].  \mforall{}[n:\mBbbN{}].    reverse\_select(l;n)  \mmember{}  T  supposing  n  <  ||l||


By

---

Latex:
(Unfold  `reverse\_select`  0  THEN  Auto')

---

Home Index