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