proposition: Lemma wp_sound: forall prog post, synt_wp prog post |= prog{=post=}.
proof: Proof. intros prog post e H0 e' H; generalize post H0; clear H0 post. elim H; clear H e' e prog; simpl; try ((firstorder eauto 20 with hoare); fail). intros e cond p1 p2 e'. case (E.eval cond e); simpl; firstorder auto. Qed.
imports: hoarelogicsemantics