proposition: Lemma triple_consequence: forall P Q P' Q' c, {{P}} c {{Q}} -> P' -->> P -> Q -->> Q' -> {{P'}} c {{Q'}}.
proof: Proof. unfold triple, aimp; intros. eauto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)