proposition: Lemma triple_assign_fwd: forall x a P, {{ P }} ASSIGN x a {{ aexists (fun m => aexists (fun n => aequal (VAR x) n //\\ aupdate x (CONST m) (P //\\ aequal a n))) }}.
proof: Proof. intros. unfold triple, aequal, aupdate; intros. inversion H; subst. exists (s x); exists (aeval a s); cbn. split. apply update_same. replace (update x (s x) (update x (aeval a s) s)) with s. split; auto. apply functional_extensionality; intros y. unfold update. destruct (string_dec x y); congruence. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)