---

Step * of Lemma mon_nat_op_zero

∀[g:IMonoid]. ∀[e:|g|].  ((0 ⋅ e) = e ∈ |g|)
BY
{ ProveSpecializedLemma `nat_op_zero` 0 [parm{i}] (FoldC `mon_nat_op`) }

---

Latex:

---

Latex:
\mforall{}[g:IMonoid].  \mforall{}[e:|g|].    ((0  \mcdot{}  e)  =  e)


By

---

Latex:
ProveSpecializedLemma  `nat\_op\_zero`  0  [parm\{i\}]  (FoldC  `mon\_nat\_op`)

---

Home Index