---

Step * of Lemma minus-monomial_wf

∀[m:iMonomial()]. (minus-monomial(m) ∈ iMonomial())
BY
{ (Unfold `iMonomial` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[m:iMonomial()].  (minus-monomial(m)  \mmember{}  iMonomial())


By

---

Latex:
(Unfold  `iMonomial`  0  THEN  ProveWfLemma)

---

Home Index