---

Step * of Lemma radd-list-one

∀[L:Top List]. (radd-list(map(λk.r1;L)) = r(||L||))
BY
{ (InductionOnList THEN Reduce 0 THEN RWW "radd-list-cons -1 radd-int" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L:Top  List].  (radd-list(map(\mlambda{}k.r1;L))  =  r(||L||))


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  RWW  "radd-list-cons  -1  radd-int"  0  THEN  Auto)

---

Home Index