vs : forall c (v:V) Q, eval vs (addX c v Q) = phi c * vs v + eval vs Q. Proof. intros. unfold addX. pose proof (decide_eqb_ok c 0) as E. destruct (c =? 0). - rewrite (fst E) by split. rewrite (preserves_0 (f:=phi)). rewrite mult_0_l,plus_0_l. split. - apply '. Qed.
Require Import Import Quoting.