proposition: Lemma eval_PXguard vs : forall P (v:V) Q, eval vs (PXguard P v Q) = eval vs P * vs v + eval vs Q.
proof: 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.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.additional_operations HoTT.Classes.tactics.ring_quote HoTT.Classes.theory.rings