---

Step * of Lemma poly-int_wf

∀[p:tree(ℤ)]. (poly-int(p) ∈ 𝔹)
BY
{ (Intro THEN Unfold `poly-int` 0 THEN Using [`E',⌜ℤ⌝] MemCD⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p:tree(\mBbbZ{})].  (poly-int(p)  \mmember{}  \mBbbB{})


By

---

Latex:
(Intro  THEN  Unfold  `poly-int`  0  THEN  Using  [`E',\mkleeneopen{}\mBbbZ{}\mkleeneclose{}]  MemCD\mcdot{}  THEN  Auto)

---

Home Index