---

Step * of Lemma mul-list-append

∀[ns1,ns2:ℤ List].  (Π(ns1 @ ns2)  ~ Π(ns1)  * Π(ns2) )
BY
{ xxx(InductionOnList THEN Reduce 0)xxx }

1
∀[ns2:ℤ List]. (Π(ns2)  ~ 1 * Π(ns2) )

2
1. u : ℤ
2. v : ℤ List
3. ∀[ns2:ℤ List]. (Π(v @ ns2)  ~ Π(v)  * Π(ns2) )
⊢ ∀[ns2:ℤ List]. (Π([u / (v @ ns2)])  ~ Π([u / v])  * Π(ns2) )

---

Latex:

---

Latex:
\mforall{}[ns1,ns2:\mBbbZ{}  List].    (\mPi{}(ns1  @  ns2)    \msim{}  \mPi{}(ns1)    *  \mPi{}(ns2)  )


By

---

Latex:
xxx(InductionOnList  THEN  Reduce  0)xxx

---

Home Index