Commit 3e4b87c2 authored by Robbert Krebbers's avatar Robbert Krebbers

Show that bupd entails plausibly.

parent 5b084890
...@@ -172,6 +172,12 @@ Section bupd_derived_sbi. ...@@ -172,6 +172,12 @@ Section bupd_derived_sbi.
- rewrite -bupd_intro. apply forall_intro=> x. - rewrite -bupd_intro. apply forall_intro=> x.
by rewrite (forall_elim x) bupd_plain. by rewrite (forall_elim x) bupd_plain.
Qed. Qed.
Lemma bupd_plausibly P : (|==> P) <plausible> P.
Proof.
apply forall_intro=> Q. apply wand_intro_l. rewrite bupd_frame_l.
by rewrite plainly_elim wand_elim_l bupd_plain.
Qed.
End bupd_plainly. End bupd_plainly.
End bupd_derived_sbi. End bupd_derived_sbi.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment