proposition: Lemma triple_get: forall x a l v, [[ aequal a l //\\ contains l v ]] GET x a [[ aequal (VAR x) v //\\ contains l v ]].
proof: Proof. intros; intros R IND s h (h1 & h2 & (P1 & P2) & R1 & DISJ & EQ). do 2 econstructor; split. - apply star_one. apply red_get with (l := l) (v := v); auto. rewrite EQ, P2; cbn. destruct (Z.eq_dec l l); congruence. - exists h1, h2; intuition auto. + split. red; cbn. apply 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)