diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index e270d09ae98b24f3e4a714256718879aa48b0c72..5b4c19f5f6aef09c317b2078d824836cf7ded31a 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -248,7 +248,7 @@ Proof.
   - by destruct 1; simpl; intros ?; setoid_subst.
   - by intros ? [|]; destruct 1; inversion_clear 1; econstructor; setoid_subst.
   - destruct 3; simpl in *; destruct_and?; eauto using closed_op;
-      match goal with H : closed _ _ |- _ => destruct H end; set_solver.
+      select (closed _ _) (fun H => destruct H); set_solver.
   - intros []; naive_solver eauto using closed_up, closed_up_set,
       elem_of_up, elem_of_up_set with sts.
   - intros [] [] [] _ _ _ _ _; constructor; rewrite ?assoc; auto with sts.
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index eca1b60943b0ab91b4b7762c649f8266cb3c43c5..78bcee3fc53f9ffe6c542d1b8838b6d02864eac9 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -34,7 +34,7 @@ Section modalities.
       (MIEnvFilter Objective) (MIEnvFilter Objective).
   Proof.
     split; simpl; split_and?; intros;
-      try match goal with H : TCDiag _ _ _ |- _ => destruct H end;
+      try select (TCDiag _ _ _) (fun H => destruct H);
       eauto using bi.equiv_entails_sym, objective_objectively,
         monPred_objectively_mono, monPred_objectively_and,
         monPred_objectively_sep_2 with typeclass_instances.