Commit f2450784 authored by Robbert Krebbers's avatar Robbert Krebbers

Put now_True_rvs near derived properties (since it _is_ derived).

parent 1c0a0e04
Pipeline #2632 passed with stage
in 8 minutes and 53 seconds
......@@ -1181,11 +1181,6 @@ Proof.
exists (y x3); split; first by rewrite -assoc.
exists y; eauto using cmra_includedN_l.
Qed.
Lemma now_True_rvs P : (|=r=> P) (|=r=> P).
Proof.
rewrite /uPred_now_True. apply or_elim; auto using rvs_mono.
by rewrite -rvs_intro -or_intro_l.
Qed.
(** * Derived rules *)
Global Instance rvs_mono' : Proper (() ==> ()) (@uPred_rvs M).
......@@ -1205,6 +1200,11 @@ Proof.
intros; rewrite (rvs_ownM_updateP _ (y =)); last by apply cmra_update_updateP.
by apply rvs_mono, exist_elim=> y'; apply pure_elim_l=> ->.
Qed.
Lemma now_True_rvs P : (|=r=> P) (|=r=> P).
Proof.
rewrite /uPred_now_True. apply or_elim; auto using rvs_mono.
by rewrite -rvs_intro -or_intro_l.
Qed.
(* Products *)
Lemma prod_equivI {A B : cofeT} (x y : A * B) : x y ⊣⊢ x.1 y.1 x.2 y.2.
......
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