diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index f03509b43dfe354077708e44c46fa00b66982042..fb5b5de765a64fb0ab5123e0e276f66f6bba1963 100644
--- 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.