eval_add' vs : forall P Q, eval vs (add P Q) = eval vs P + eval vs Q. Proof. induction P as [c|P1 IH1 v P2 IH2];intros Q. - simpl. apply eval_addC. - simpl. rewrite eval_add_aux;auto. rewrite IH2. apply plus_assoc. Qed.
Require Import Import Quoting.