---

Step * 2 of Lemma mul-list-append


1. u : ℤ
2. v : ℤ List
3. ∀[ns2:ℤ List]. (Π(v @ ns2)  ~ Π(v)  * Π(ns2) )
⊢ ∀[ns2:ℤ List]. (Π([u / (v @ ns2)])  ~ Π([u / v])  * Π(ns2) )
BY
{ xxx(Unfold `mul-list` 0 THEN Reduce 0 THEN Fold `mul-list` 0 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
3.  \mforall{}[ns2:\mBbbZ{}  List].  (\mPi{}(v  @  ns2)    \msim{}  \mPi{}(v)    *  \mPi{}(ns2)  )
\mvdash{}  \mforall{}[ns2:\mBbbZ{}  List].  (\mPi{}([u  /  (v  @  ns2)])    \msim{}  \mPi{}([u  /  v])    *  \mPi{}(ns2)  )


By

---

Latex:
xxx(Unfold  `mul-list`  0  THEN  Reduce  0  THEN  Fold  `mul-list`  0  THEN  Auto)xxx

---

Home Index