---

Step * of Lemma const-poly_wf

∀[n:ℤ-o]. (const-poly(n) ∈ iPolynomial())
BY
{ (Unfold `iPolynomial` 0 THEN ProveWfLemma THEN MemTypeCD THEN Auto') }

1
.....subterm..... T:t
2:n
1. n : ℤ-o
⊢ [] ∈ {vs:ℤ List| sorted(vs)} 

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}\msupminus{}\msupzero{}].  (const-poly(n)  \mmember{}  iPolynomial())


By

---

Latex:
(Unfold  `iPolynomial`  0  THEN  ProveWfLemma  THEN  MemTypeCD  THEN  Auto')

---

Home Index