proposition: Lemma triple_frame: forall c P Q R, {{P}} c {{Q}} -> independent_of R (modified_by c) -> {{P //\\ R}} c {{Q //\\ R}}.
proof: Proof. intros; red; intros. destruct H2 as [PRE1 PRE2]. split. - eapply H; eauto. - apply (H0 s' s). + intros. apply cexec_modified with c; auto. + auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)