---

Step * of Lemma nat_op_wf

∀[g:IMonoid]. ∀[n:ℕ]. ∀[e:|g|].  (n x(*;e) e ∈ |g|)
BY
{ Unfold `nat_op` 0 THEN Auto }

---

Latex:

---

Latex:
\mforall{}[g:IMonoid].  \mforall{}[n:\mBbbN{}].  \mforall{}[e:|g|].    (n  x(*;e)  e  \mmember{}  |g|)


By

---

Latex:
Unfold  `nat\_op`  0  THEN  Auto

---

Home Index