---

Step * of Lemma radd-as-radd-list

∀[a,b:ℝ].  ((a + b) = radd-list([a; b]) ∈ ℝ)
BY
{ (Auto THEN RepUR ``radd-list`` 0 THEN (CallByValueReduce 0 THENA Auto) THEN (Reduce 0 THEN Fold `radd` 0 THEN Auto)) }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbR{}].    ((a  +  b)  =  radd-list([a;  b]))


By

---

Latex:
(Auto
  THEN  RepUR  ``radd-list``  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (Reduce  0  THEN  Fold  `radd`  0  THEN  Auto))

---

Home Index