---

Step * of Lemma select-is-bottom

∀[X:Top List]. ∀[i:ℕ].  X[i] ~ ⊥ supposing ||X|| ≤ i
BY
{ (InductionOnList THEN Reduce 0 THEN Auto) }

1
1. u : Top
2. v : Top List
3. ∀[i:ℕ]. v[i] ~ ⊥ supposing ||v|| ≤ i
4. i : ℕ
5. (||v|| + 1) ≤ i
⊢ [u / v][i] ~ ⊥

---

Latex:

---

Latex:
\mforall{}[X:Top  List].  \mforall{}[i:\mBbbN{}].    X[i]  \msim{}  \mbot{}  supposing  ||X||  \mleq{}  i


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto)

---

Home Index