---

Step * 1 1 1 of Lemma mul-mono-poly_wf


1. m : iMonomial()
⊢ (∀i:ℕ0. ∀j:ℕi.  imonomial-less(⊥;⊥)) ⇒ (∀i:ℕ0. ∀j:ℕi.  imonomial-less(⊥;⊥))
BY
{ Auto }

---

Latex:

---

Latex:

1.  m  :  iMonomial()
\mvdash{}  (\mforall{}i:\mBbbN{}0.  \mforall{}j:\mBbbN{}i.    imonomial-less(\mbot{};\mbot{}))  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}0.  \mforall{}j:\mBbbN{}i.    imonomial-less(\mbot{};\mbot{}))


By

---

Latex:
Auto

---

Home Index