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