proposition: Lemma triple_set: forall a1 a2 l v, [[ aequal a1 l //\\ aequal a2 v //\\ valid l ]] SET a1 a2 [[ contains l v ]].
proof: Proof. intros; intros R IND s h (h1 & h2 & (P1 & P2 & P3) & R1 & DISJ & EQ). destruct P3 as (v0 & P3). do 2 econstructor; split. - apply star_one. eapply red_set with (l := l) (v := v); auto. rewrite EQ, P3. cbn. destruct (Z.eq_dec l l); congruence. - exists (hupdate l v hempty), h2; intuition auto. + red; auto. + intros l'. specialize (DISJ l'). rewrite P3 in DISJ. cbn in *. destruct (Z.eq_dec l l'); intuition congruence. + rewrite EQ, P3. apply heap_extensionality; intros l'; cbn. destruct (Z.eq_dec l l'); auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)