eval_0' : forall P, P =? 0 = true -> forall vs, eval vs P = 0. Proof. induction P;simpl;intros E vs. - change eqb with Peqb in E;simpl in E. apply decide_eqb_ok in E. rewrite E. apply preserves_0. - change eqb with Peqb in E;simpl in E. destruct (false_ne_true E). Qed.
Require Import Import Quoting.