proposition: Lemma wp_entails_wlp: forall prog post, prog [= post =] |= prog {= post =}.
proof: Proof. unfold wp, wlp. intros prog post e H e' H'. dec2 e0 H. dec2 H0 H. rewrite (exec_deterministic H' H0). auto. Qed.
imports: hoarelogicsemantics partialhoarelogic totalhoarelogic