proposition: Lemma triple_consequence: forall P P' c Q' Q, P -->> P' -> [[ P' ]] c [[ Q' ]] -> Q' -->> Q -> [[ P ]] c [[ Q ]].
proof: Proof. intros; intros R IND s h PRE. destruct (H0 R IND s h) as (s' & h' & EXEC & POST). apply aimp_sepconj with P; auto. exists s', h'; split; auto. apply aimp_sepconj with Q'; auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)