---

Step * 1 of Lemma firstn_map_upto


∀[n:ℕ]. ([] ~ map(λi.⊥;upto(imin(0;n))))
BY
{ (D 0 THENA Auto) }

1
1. n : ℕ
⊢ [] ~ map(λi.⊥;upto(imin(0;n)))

---

Latex:

---

Latex:

\mforall{}[n:\mBbbN{}].  ([]  \msim{}  map(\mlambda{}i.\mbot{};upto(imin(0;n))))


By

---

Latex:
(D  0  THENA  Auto)

---

Home Index