vs : forall P (v:V) Q, eval vs (PXguard P v Q) = eval vs P * vs v + eval vs Q. Proof. intros. unfold PXguard. pose proof (eval_0 P) as E. destruct (P =? 0). - rewrite E by split. rewrite mult_0_l,plus_0_l. split. - reflexivity. Qed.
Require Import Import Quoting.