diff --git a/example_relabeling.v b/example_relabeling.v
index 24505fa..98e53b8 100644
--- a/example_relabeling.v
+++ b/example_relabeling.v
@@ -89,7 +89,7 @@ transitivity (do x0 <- relabel u;
             (do x <- assert q x1; (Ret \o ucat) x));
    m x0 x))%Do; last first.
   bind_ext => u'; rewrite bind_fmap bindA; bind_ext => sS.
-  rewrite 4!bindA; bind_ext => x; rewrite 2!bindretf !bindA.
+  rewrite 4!bindA; bind_ext => x; rewrite 2!bindretf bindA.
   by under eq_bind do rewrite bindretf.
 rewrite -H1.
 rewrite [in LHS]/drBin bind_fmap [in LHS]/bassert /= ![in LHS]bindA.
diff --git a/fail_lib.v b/fail_lib.v
index d06fa79..144ae31 100644
--- a/fail_lib.v
+++ b/fail_lib.v
@@ -1431,7 +1431,7 @@ Lemma guard_splits {T A : UU0} (p : pred T) (t : seq T) (f : seq T * seq T -> M
   splits t >>= (fun x => guard (all p x.1) >> guard (all p x.2) >> f x).
 Proof.
 rewrite -plus_commute//.
-elim: t => [|h t ih] in p f *; first by rewrite 2!bindretf guardT bindmskip.
+elim: t => [|h t ih] in p f *; first by rewrite /= !bindretf.
 rewrite [LHS]/= guard_and 2!bindA ih /= plus_commute//.
 rewrite bindA; bind_ext => -[a b] /=.
 rewrite !alt_bindDl !bindretf /= !guard_and !bindA !alt_bindDr.
diff --git a/hier.png b/hier.png
index c804af5..8173740 100644
Binary files a/hier.png and b/hier.png differ
diff --git a/hierarchy.v b/hierarchy.v
index e6cb85a..4c5d866 100644
--- a/hierarchy.v
+++ b/hierarchy.v
@@ -721,27 +721,26 @@ Arguments fail {_} {_}.
 Section guard_assert.
 Variable M : failMonad.
 
-Definition guard (b : bool) : M unit := locked (if b then skip else fail).
+Definition guard (b : bool) : M unit := if b then skip else fail.
 
 Lemma guardPn (b : bool) : if_spec b skip fail (~~ b) b (guard b).
-Proof. by rewrite /guard; unlock; case: ifPn => ?; constructor. Qed.
+Proof. by rewrite /guard; case: ifPn => ?; constructor. Qed.
 
-Lemma guardT : guard true = skip. Proof. by rewrite /guard; unlock. Qed.
+Lemma guardT : guard true = skip. Proof. by []. Qed.
 
-Lemma guardF : guard false = fail. Proof. by rewrite /guard; unlock. Qed.
+Lemma guardF : guard false = fail. Proof. by []. Qed.
 
 (* guard distributes over conjunction *)
 Lemma guard_and a b : guard (a && b) = guard a >> guard b.
 Proof.
-move: a b => -[|] b /=; by [rewrite guardT bindskipf | rewrite guardF bindfailf].
+by move: a b => -[|] b /=; [rewrite bindskipf | rewrite bindfailf].
 Qed.
 
-Definition assert {A : UU0} (p : pred A) (a : A) : M A :=
-  locked (guard (p a) >> Ret a).
+Definition assert {A : UU0} (p : pred A) (a : A) : M A := guard (p a) >> Ret a.
 
 Lemma assertE {A : UU0} (p : pred A) (a : A) :
   assert p a = guard (p a) >> Ret a.
-Proof. by rewrite /assert; unlock. Qed.
+Proof. by []. Qed.
 
 Lemma assertT {A : UU0} (a : A) : assert xpredT a = Ret a.
 Proof. by rewrite assertE guardT bindskipf. Qed.
@@ -778,8 +777,8 @@ case: guardPn => Hb.
 Qed.
 
 End guard_assert.
-Arguments assert {M} {A}.
-Arguments guard {M}.
+Arguments assert {M} {A} : simpl never.
+Arguments guard {M} : simpl never.
 
 HB.mixin Record isMonadAlt (M : UU0 -> UU0) of Monad M := {
   alt : forall T : UU0, M T -> M T -> M T ;
@@ -824,8 +823,7 @@ HB.mixin Record isMonadNondet (M : UU0 -> UU0) of MonadFail M & MonadAlt M := {
   altmfail : @BindLaws.right_id M (@fail M) (@alt M) }.
 
 #[short(type=nondetMonad)]
-HB.structure Definition MonadNondet :=
-  {M of isMonadNondet M & MonadFail M & MonadAlt M}.
+HB.structure Definition MonadNondet := {M of isMonadNondet M & }.
 
 #[short(type=nondetCIMonad)]
 HB.structure Definition MonadCINondet := {M of MonadAltCI M & MonadNondet M}.
@@ -1074,7 +1072,7 @@ HB.mixin Record isMonadArray (S : UU0) (I : eqType) (M : UU0 -> UU0)
 
 #[short(type=arrayMonad)]
 HB.structure Definition MonadArray (S : UU0) (I : eqType) :=
-  { M of isMonadArray S I M & isMonad M & isFunctor M }.
+  { M of isMonadArray S I M & }.
 
 #[short(type=plusArrayMonad)]
 HB.structure Definition MonadPlusArray (S : UU0) (I : eqType) :=
@@ -1311,8 +1309,7 @@ HB.mixin Record isMonadAltProb {R : realType} (M : UU0 -> UU0)
 
 #[short(type=altProbMonad)]
 HB.structure Definition MonadAltProb {R : realType} :=
-  { M of isMonadAltProb R M & isFunctor M & isMonad M & isMonadAlt M &
-         isMonadAltCI M & isMonadProb R M & isMonadConvex R M }.
+  { M of isMonadAltProb R M & }.
 
 Section altprob_lemmas.
 Context {R : realType}.
diff --git a/impredicative_set/ifail_lib.v b/impredicative_set/ifail_lib.v
index aefa647..2898df0 100644
--- a/impredicative_set/ifail_lib.v
+++ b/impredicative_set/ifail_lib.v
@@ -25,7 +25,7 @@ From Equations Require Import Equations.
 (*                          defined as a Fixpoint using insert [1, Sect. 3]   *)
 (*              select s == nondeterministically splits the list s into a     *)
 (*                          pair of one chosen element and the rest           *)
-(*                       [2, Sect. 3.2]                                       *)
+(*                          [3, Sect. 4.4] [2, Sect. 3.2]                     *)
 (*               uperm s == nondeterministically computes a permutation of s, *)
 (*                          defined using unfoldM and select [2, Sect. 3.2]   *)
 (*              splits s == split a list nondeterministically                 *)
diff --git a/impredicative_set/ihierarchy.v b/impredicative_set/ihierarchy.v
index 8909fd1..1545574 100644
--- a/impredicative_set/ihierarchy.v
+++ b/impredicative_set/ihierarchy.v
@@ -701,27 +701,27 @@ Arguments fail {_} {_}.
 Section guard_assert.
 Variable M : failMonad.
 
-Definition guard (b : bool) : M unit := locked (if b then skip else fail).
+Definition guard (b : bool) : M unit := if b then skip else fail.
 
 Lemma guardPn (b : bool) : if_spec b skip fail (~~ b) b (guard b).
-Proof. by rewrite /guard; unlock; case: ifPn => ?; constructor. Qed.
+Proof. by rewrite /guard; case: ifPn => ?; constructor. Qed.
 
-Lemma guardT : guard true = skip. Proof. by rewrite /guard; unlock. Qed.
+Lemma guardT : guard true = skip. Proof. by []. Qed.
 
-Lemma guardF : guard false = fail. Proof. by rewrite /guard; unlock. Qed.
+Lemma guardF : guard false = fail. Proof. by []. Qed.
 
 (* guard distributes over conjunction *)
 Lemma guard_and a b : guard (a && b) = guard a >> guard b.
 Proof.
-move: a b => -[|] b /=; by [rewrite guardT bindskipf | rewrite guardF bindfailf].
+by move: a b => -[|] b /=; [rewrite bindskipf | rewrite bindfailf].
 Qed.
 
 Definition assert {A : UU0} (p : pred A) (a : A) : M A :=
-  locked (guard (p a) >> Ret a).
+  guard (p a) >> Ret a.
 
 Lemma assertE {A : UU0} (p : pred A) (a : A) :
   assert p a = guard (p a) >> Ret a.
-Proof. by rewrite /assert; unlock. Qed.
+Proof. by []. Qed.
 
 Lemma assertT {A : UU0} (a : A) : assert xpredT a = Ret a.
 Proof. by rewrite assertE guardT bindskipf. Qed.
@@ -758,8 +758,8 @@ case: guardPn => Hb.
 Qed.
 
 End guard_assert.
-Arguments assert {M} {A}.
-Arguments guard {M}.
+Arguments assert {M} {A} : simpl never.
+Arguments guard {M} : simpl never.
 
 HB.mixin Record isMonadAlt (M : UU0 -> UU0) of Monad M := {
   alt : forall T : UU0, M T -> M T -> M T ;
@@ -804,8 +804,7 @@ HB.mixin Record isMonadNondet (M : UU0 -> UU0) of MonadFail M & MonadAlt M := {
   altmfail : @BindLaws.right_id M (@fail M) (@alt M) }.
 
 #[short(type=nondetMonad)]
-HB.structure Definition MonadNondet :=
-  {M of isMonadNondet M & MonadFail M & MonadAlt M}.
+HB.structure Definition MonadNondet := {M of isMonadNondet M & }.
 
 #[short(type=nondetCIMonad)]
 HB.structure Definition MonadCINondet := {M of MonadAltCI M & MonadNondet M}.
@@ -1054,7 +1053,7 @@ HB.mixin Record isMonadArray (S : UU0) (I : eqType) (M : UU0 -> UU0)
 
 #[short(type=arrayMonad)]
 HB.structure Definition MonadArray (S : UU0) (I : eqType) :=
-  { M of isMonadArray S I M & isMonad M & isFunctor M }.
+  { M of isMonadArray S I M & }.
 
 #[short(type=plusArrayMonad)]
 HB.structure Definition MonadPlusArray (S : UU0) (I : eqType) :=