ElimModal instance for □.

855014ca · Robbert Krebbers · 634fdbb6 · 855014ca
Commit 855014ca authored Oct 28, 2016 by Robbert Krebbers
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -381,6 +381,9 @@ Proof.
  rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
 Qed.

+Global Instance elim_modal_always P Q : ElimModal (□ P) P Q Q.
+Proof. intros. by rewrite /ElimModal always_elim wand_elim_r. Qed.
+
 Global Instance elim_modal_bupd P Q : ElimModal (|==> P) P (|==> Q) (|==> Q).
 Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.