---

Step * 1 of Lemma mul-list-append


∀[ns2:ℤ List]. (Π(ns2)  ~ 1 * Π(ns2) )
BY
{ Auto }

---

Latex:

---

Latex:

\mforall{}[ns2:\mBbbZ{}  List].  (\mPi{}(ns2)    \msim{}  1  *  \mPi{}(ns2)  )


By

---

Latex:
Auto

---

Home Index