diff --git a/UniMath/CategoryTheory/Monoidal/DisplayedCartesianMonoidalCategoriesWhiskered.v b/UniMath/CategoryTheory/Monoidal/DisplayedCartesianMonoidalCategoriesWhiskered.v
index 1e257ea4d7..3a5ad58cdd 100644
--- a/UniMath/CategoryTheory/Monoidal/DisplayedCartesianMonoidalCategoriesWhiskered.v
+++ b/UniMath/CategoryTheory/Monoidal/DisplayedCartesianMonoidalCategoriesWhiskered.v
@@ -32,6 +32,8 @@ Require Import UniMath.CategoryTheory.Monoidal.DisplayedMonoidalWhiskered.
 
 Require Import UniMath.CategoryTheory.Monoidal.CartesianMonoidalCategoriesWhiskered.
 
+Require Export UniMath.Tactics.EnsureStructuredProofs.
+
 Local Open Scope cat.
 Local Open Scope mor_disp_scope.
 
@@ -277,8 +279,6 @@ Section FixADisplayedCategory.
     - exact DCM_associatorinv_data.
   Defined.
 
-Set Default Goal Selector "1".
-
   Lemma DCM_leftunitor_law : disp_leftunitor_law DCM_leftunitor_data DCM_leftunitorinv_data.
   Proof.
     split; [| split]; try red; intros.
@@ -297,9 +297,8 @@ Set Default Goal Selector "1".
       (* eapply (pathscomp0(b:=?[sh1])).
       Show sh1. *)
       etrans.
-      2: { simple refine (dispBinProduct_endo_is_identity _ _ _ _ _ _ ?[shH1] _ ?[shH2] _). shelve. (* creates one shelved goal *)
+      2: { refine (dispBinProduct_endo_is_identity _ _ _ _ _ _ ?[shH1] _ ?[shH2] _). (* creates one shelved goal *)
            + apply dispTerminalArrowEq. (* resolves the shelved goal *)
-           + shelve. (* creates one shelved goal *)
            + rewrite assoc_disp_var.
              rewrite dispBinProductPr2Commutes.
              apply pathsinv0, transportf_comp_lemma.
@@ -329,7 +328,7 @@ Set Default Goal Selector "1".
     - cbn. unfold DCM_rightunitorinv_data, DCM_rightunitor_data.
       apply pathsinv0.
       etrans.
-      2: { simple refine (dispBinProduct_endo_is_identity _ _ _ _ _ _ ?[shH1] _ ?[shH2] _). shelve. (* creates one shelved goal *)
+      2: { refine (dispBinProduct_endo_is_identity _ _ _ _ _ _ ?[shH1] _ ?[shH2] _). (* creates one shelved goal *)
            (* Show shH1. *)
            + rewrite assoc_disp_var.
              rewrite dispBinProductPr1Commutes.
@@ -339,7 +338,6 @@ Set Default Goal Selector "1".
              rewrite transport_f_b.
              apply transportf_comp_lemma.
              apply transportf_comp_lemma_hset; try apply homset_property; apply idpath.
-           + shelve. (* creates one shelved goal *)
            + apply dispTerminalArrowEq. (* resolves second shelved goal *)
              (* Show shH1. *)
       }
@@ -349,8 +347,6 @@ Set Default Goal Selector "1".
       rewrite <- assoc. rewrite BinProductPr1Commutes. apply id_right.
   Qed.
 
-Export Set Default Goal Selector "!".
-
   Lemma DCM_associator_law : disp_associator_law DCM_associator_data DCM_associatorinv_data.
   Proof.
     repeat split; try red; intros.