---

Step * of Lemma l_sum-append

∀[L1,L2:ℤ List].  (l_sum(L1 @ L2) ~ l_sum(L1) + l_sum(L2))
BY
{ ((InductionOnList THEN Auto) THEN RepUR ``l_sum`` 0 THEN Fold `l_sum` 0 THEN Auto' THEN RWO "-2" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L1,L2:\mBbbZ{}  List].    (l\_sum(L1  @  L2)  \msim{}  l\_sum(L1)  +  l\_sum(L2))


By

---

Latex:
((InductionOnList  THEN  Auto)
  THEN  RepUR  ``l\_sum``  0
  THEN  Fold  `l\_sum`  0
  THEN  Auto'
  THEN  RWO  "-2"  0
  THEN  Auto)

---

Home Index