proposition: Lemma triple_free: forall a l, [[ aequal a l //\\ valid l ]] FREE a [[ emp ]].
proof: Proof. intros; intros R IND s h (h1 & h2 & (P1 & P2) & R1 & DISJ & EQ). destruct P2 as (v0 & P2). do 2 econstructor; split. - apply star_one. apply red_free with (l := l); auto. rewrite EQ; cbn. rewrite ! P2, hupdate_same. congruence. - exists hempty, h2; intuition auto. + red; auto. + red; auto. + rewrite EQ, P2. apply heap_extensionality; intros l'; cbn. destruct (Z.eq_dec l l'); auto. subst l'. generalize (DISJ l). rewrite P2, hupdate_same. intuition congruence. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)