---

Step * of Lemma firstn-mklist1

∀[m,n:ℕ]. ∀[f:ℕm ⟶ Top].  ((n ≤ m) ⇒ (firstn(n;mklist(m;f)) ~ mklist(n;f)))
BY
{ Auto }

1
1. m : ℕ
2. n : ℕ
3. f : ℕm ⟶ Top
4. n ≤ m
⊢ firstn(n;mklist(m;f)) ~ mklist(n;f)

---

Latex:

---

Latex:
\mforall{}[m,n:\mBbbN{}].  \mforall{}[f:\mBbbN{}m  {}\mrightarrow{}  Top].    ((n  \mleq{}  m)  {}\mRightarrow{}  (firstn(n;mklist(m;f))  \msim{}  mklist(n;f)))


By

---

Latex:
Auto

---

Home Index