proposition: Lemma eval_pol_norm : forall env lhs, eval_pexpr env lhs == eval_pol env (norm lhs).
proof: Proof. intros. apply (norm_aux_spec (SORsetoid sor) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor)) (SORrm addon) (SORpower addon) ). Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl