diff --git a/rt/analysis/WCET_is_pWCET.v b/rt/analysis/WCET_is_pWCET.v
index 4d2887351588cd318e56b53e3646611757b8954d..eb039850d5a6489f84883e4b91e8213803f37545 100644
--- a/rt/analysis/WCET_is_pWCET.v
+++ b/rt/analysis/WCET_is_pWCET.v
@@ -145,5 +145,3 @@ Section WCETisAxiomaticPWCET.
   Qed.
 
 End WCETisAxiomaticPWCET.
-
-Print Assumptions WCET_is_axiomatic_pWCET.
diff --git a/rt/analysis/axiomatic_pWCET_full.v b/rt/analysis/axiomatic_pWCET_full.v
index e8aeb0774bbc7c4f21e555aa215823e2ef1b8d3c..2924fef1bdb7a2ca38726ccad707908f182f1676 100644
--- a/rt/analysis/axiomatic_pWCET_full.v
+++ b/rt/analysis/axiomatic_pWCET_full.v
@@ -105,5 +105,3 @@ Section MainLemma.
   Qed.
 
 End MainLemma.
-
-Print Assumptions probabilistic_rt_monotonicity_of_iid_pWCET.
diff --git a/rt/analysis/pRTA/pRTA.v b/rt/analysis/pRTA/pRTA.v
index 47e83d188337c30c4ca5c4f77763f259b8be6f8e..fca5a2e4c29197997ccf1ea432344c0da6ba7411 100644
--- a/rt/analysis/pRTA/pRTA.v
+++ b/rt/analysis/pRTA/pRTA.v
@@ -470,5 +470,3 @@ Section WCDFPIsBounded.
   Qed.
 
 End WCDFPIsBounded.
-
-Print Assumptions probabilistic_rta_fp.
diff --git a/rt/analysis/work_bound.v b/rt/analysis/work_bound.v
index fb98d26433e44e97eaa7e52a5775751cde99a9a9..975d34e8ddf17d20ff1785ea71c7396f7fb8a0e8 100644
--- a/rt/analysis/work_bound.v
+++ b/rt/analysis/work_bound.v
@@ -33,9 +33,9 @@ Section PrTaskWorkloadBoundedNthCost.
 
   (** Assume that job costs are independent of the (prob.) arrival sequence. *)
   Let ξpart := partition_on_ξ μ : Ω_partition.
-  Hypothesis job_costs_independent_arr_seq :
+  Hypothesis H_job_costs_independent_arr_seq :
     let ξpart := partition_on_ξ μ : Ω_partition in
-    forall (ξ : I ξpart) `{!PosProb μ (ξpart◁{ξ})} (jobs : seq Job),
+    forall (ξ : I ξpart) `(!PosProb μ (ξpart◁{ξ})) (jobs : seq Job),
       indep2
         (mkRvar μ (fun ω => [seq job_cost j ω | j <- jobs]))
         (mkRvar μ (fun ω => ξpart◁{ξ} ω)).
@@ -61,7 +61,7 @@ Section PrTaskWorkloadBoundedNthCost.
       { by rewrite //= in IHjobs; rewrite //= !big_cons //= IHjobs. }
     }
     eapply indep2_fn_extl; first by intros; apply: EQ.
-    by apply job_costs_independent_arr_seq, PosProb0.
+    by apply H_job_costs_independent_arr_seq, PosProb0.
   Qed.