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