---

Step * of Lemma valueall-type-polynom

∀[n:ℕ]. valueall-type(polynom(n))
BY
{ (Auto THEN InstLemma `subtype-valueall-type` [⌜polynom(n)⌝;⌜polyform(n)⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  valueall-type(polynom(n))


By

---

Latex:
(Auto  THEN  InstLemma  `subtype-valueall-type`  [\mkleeneopen{}polynom(n)\mkleeneclose{};\mkleeneopen{}polyform(n)\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index