---

Step * 1 1 of Lemma poly-zero-val


1. p1 : ℤ
2. ↑(p1 =z 0)
3. l : Top
⊢ tree_leaf(p1)@l = 0 ∈ ℤ
BY
{ ((Fold `polyconst` 0 THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:

1.  p1  :  \mBbbZ{}
2.  \muparrow{}(p1  =\msubz{}  0)
3.  l  :  Top
\mvdash{}  tree\_leaf(p1)@l  =  0


By

---

Latex:
((Fold  `polyconst`  0  THEN  Reduce  0)  THEN  Auto)

---

Home Index