proposition: Lemma wp_complete: forall prog post, prog{=post=} |= (synt_wp prog post).
proof: Proof. unfold wlp; intros prog; elim prog; clear prog; simpl; try ((firstorder auto with hoare); fail). eauto with hoare. intros. constructor 1 with (x:=wlp (Iwhile cond p) post). unfold wlp; intuition eauto 20 with hoare. Qed.
imports: hoarelogicsemantics