---

Step * of Lemma poly_int_val_cons

∀p,l,a:Top.  (p@[a / l] ~ Σ(p[i]@l * a^||p|| - 1 - i | i < ||p||))
BY
{ (UnivCD THENA Auto) }

1
1. p : Top
2. l : Top
3. a : Top
⊢ p@[a / l] ~ Σ(p[i]@l * a^||p|| - 1 - i | i < ||p||)

---

Latex:

---

Latex:
\mforall{}p,l,a:Top.    (p@[a  /  l]  \msim{}  \mSigma{}(p[i]@l  *  a\^{}||p||  -  1  -  i  |  i  <  ||p||))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index