proposition: Lemma Hoare_consequence_post: forall P Q Q' c, Hoare P c Q -> Q -->> Q' -> 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)