---

Step * 1 of Lemma unshuffle-map'


1. f : ℕ ⟶ Top
2. m : ℕ
3. r : ℕ2
4. r = 0 ∈ ℤ
⊢ unshuffle(map(f;upto((2 * m) + 0))) ~ unshuffle(map(f;upto(2 * m)))
BY
{ (RepeatFor 3 (EqCD) THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}  {}\mrightarrow{}  Top
2.  m  :  \mBbbN{}
3.  r  :  \mBbbN{}2
4.  r  =  0
\mvdash{}  unshuffle(map(f;upto((2  *  m)  +  0)))  \msim{}  unshuffle(map(f;upto(2  *  m)))


By

---

Latex:
(RepeatFor  3  (EqCD)  THEN  Auto)

---

Home Index