proposition: Lemma triple_assign: forall P x a, {{aupdate x a P}} ASSIGN x a {{P}}.
proof: Proof. unfold triple, aupdate; intros. inversion H; subst. auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)