---

Step * of Lemma select-add-indices

∀[T:Type]. ∀[L:T List]. ∀[i:ℕ||L||].  (add-indices(L)[i] = <i, L[i]> ∈ (ℕ||L|| × T))
BY
{ ((Auto THEN Unfold `add-indices` 0) THEN RWO "select-map" 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[i:\mBbbN{}||L||].    (add-indices(L)[i]  =  <i,  L[i]>)


By

---

Latex:
((Auto  THEN  Unfold  `add-indices`  0)  THEN  RWO  "select-map"  0  THEN  Reduce  0  THEN  Auto)

---

Home Index