---

Step * of Lemma polyvar-val

∀[v:ℕ]. ∀[l:{l:ℤ List| v < ||l||} ].  (polyvar(v)@l = l[v] ∈ ℤ)
BY
{ ((InductionOnNat THEN Auto) THEN RecUnfold `polyvar` 0 THEN Reduce 0) }

1
1. v : ℤ
2. l : {l:ℤ List| 0 < ||l||} 
⊢ tree_node(tree_leaf(0);tree_leaf(1))@l = l[0] ∈ ℤ

2
1. v : ℤ
2. 0 < v
3. ∀[l:{l:ℤ List| v - 1 < ||l||} ]. (polyvar(v - 1)@l = l[v - 1] ∈ ℤ)
4. l : {l:ℤ List| v < ||l||} 
⊢ if v=0  then tree_node(tree_leaf(0);tree_leaf(1))  else eval a = polyvar(v - 1) in tree_node(a;tree_leaf(0))@l
= l[v]
∈ ℤ

---

Latex:

---

Latex:
\mforall{}[v:\mBbbN{}].  \mforall{}[l:\{l:\mBbbZ{}  List|  v  <  ||l||\}  ].    (polyvar(v)@l  =  l[v])


By

---

Latex:
((InductionOnNat  THEN  Auto)  THEN  RecUnfold  `polyvar`  0  THEN  Reduce  0)

---

Home Index