diff --git a/fail_lib.v b/fail_lib.v
index 66b3645c..a18026c6 100644
--- a/fail_lib.v
+++ b/fail_lib.v
@@ -1010,6 +1010,9 @@ End splits_prePlusMonad.
 Section qperm.
 Variables (M : altMonad) (A : UU0) (d : unit) (T : orderType d).
 
+Set Printing All.
+Set Printing Universes.
+
 Equations? qperm (s : seq A) : M (seq A) by wf (size s) lt :=
 | [::] => Ret [::]
 | x :: xs =>
diff --git a/proba_monad_model.v b/proba_monad_model.v
index 29fbeab0..ba277d9c 100644
--- a/proba_monad_model.v
+++ b/proba_monad_model.v
@@ -88,7 +88,11 @@ Let choiceA : forall (T : Type) (p q r s : prob) (a b c : acto T),
     let bc := (choice q _ b c) in
     let ab := (choice r _ a b) in
     choice p _ a bc = choice s _ ab c.
-Proof. by move=> ? ? ? ? ? ? ? ? ? /=; exact: fsdist_convA. Qed.
+Proof.
+move=> ? p q r s a b c [] ? ? /=.
+rewrite /choice -/(conv p a (conv q b c)) -/(conv s (conv r a b) c).
+exact: convA0.
+Qed.
 Let prob_bindDl p :
   BindLaws.left_distributive (@hierarchy.bind [the monad of acto]) (choice p).
 Proof.