∀[p:tree(ℤ)]. ∀[l:Top]. (p@l = 0 ∈ ℤ) supposing ↑poly-zero(p)
{ Auto }
1. p : tree(ℤ)
2. ↑poly-zero(p)
3. l : Top
⊢ p@l = 0 ∈ ℤ