proposition: Lemma triple_frame: forall P c Q R, [[ P ]] c [[ Q ]] -> independent_of R (modified_by c) -> [[ P ** R ]] c [[ Q ** R ]].
proof: Proof. intros P c Q R TR INDR S INDS. rewrite ! sepconj_assoc. apply TR. intros h s1 s2 SAME (h1 & h2 & R1 & S2 & DISJ & EQ). exists h1, h2; intuition eauto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)