proposition: Lemma triple_assign: forall x a n, [[ aequal a n //\\ emp ]] ASSIGN x a [[ aequal (VAR x) n //\\ emp ]].
proof: Proof. intros; intros R IND s h (h1 & h2 & (P1 & P2) & R1 & DISJ & EQ). do 2 econstructor; split. - apply star_one. apply red_assign. - exists h1, h2; intuition auto. + split; auto. red; cbn. rewrite update_same; auto. + apply IND with s; auto. cbn; intros. apply update_other; auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)