proposition: Lemma synt_wp_monotonic: forall (p: ImpProg) (post1 post2: Pred), (forall e, post1 e -> post2 e) -> forall e, (synt_wp p post1 e) -> (synt_wp p post2 e).
proof: Proof. induction p; simpl; firstorder eauto. Qed.
imports: hoarelogicsemantics