Commit 26ae0c67 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Make iLeft and iRight work with always.

parent 37f022e4
......@@ -330,9 +330,12 @@ Proof. done. Qed.
Global Instance from_or_bupd P Q1 Q2 :
FromOr P Q1 Q2 FromOr (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /FromOr=><-. apply or_elim; apply bupd_mono; auto with I. Qed.
Global Instance from_or_always P Q1 Q2 :
FromOr P Q1 Q2 FromOr ( P) ( Q1) ( Q2).
Proof. rewrite /FromOr=> <-. by rewrite always_or. Qed.
Global Instance from_or_later P Q1 Q2 :
FromOr P Q1 Q2 FromOr ( P) ( Q1) ( Q2).
Proof. rewrite /FromOr=><-. apply or_elim; apply later_mono; auto with I. Qed.
Proof. rewrite /FromOr=><-. by rewrite later_or. Qed.
(* IntoOr *)
Global Instance into_or_or P Q : IntoOr (P Q) P Q.
......
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