proposition: Lemma Hoare_consequence_pre: forall P P' Q c, Hoare P c Q -> P' -->> P -> Hoare P' c Q.
proof: Proof. intros. apply Hoare_consequence with (P := P) (Q := Q); unfold aimp; auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)