---

Step * of Lemma value-type-polynom

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

---

Latex:

---

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


By

---

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

---

Home Index