proposition: Lemma Triple_assign: forall P x a, [[aupdate x a P]] ASSIGN x a [[P]].
proof: Proof. intros P x a s PRE. exists (update x (aeval a s) s); split. - apply cexec_assign. - exact PRE. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)