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