proposition: Lemma var_eval : forall n f v, Vector.nth v f = eval (@poly_var n f) v.
proof: Proof. Proof with autorewrite with poly_var eval in *; simpl; auto with zarith. induction f; depelim v; intros... Qed.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef