diff --git a/analysis/facts/model/ideal_uni_exceed.v b/analysis/facts/model/ideal_uni_exceed.v
index b30a00b3caf65513bbff293bd9d6790111942b07..c0465fdffd5f854c9bba7561adcb9fcee8683df4 100644
--- a/analysis/facts/model/ideal_uni_exceed.v
+++ b/analysis/facts/model/ideal_uni_exceed.v
@@ -108,8 +108,6 @@ Section ExceedanceProcStateProperties1.
     |ExceedanceExecution _ => true
     |_ => false
     end.
-  Local Transparent scheduled_in scheduled_on service_on.
-
 
   (** Next, let us consider any schedule of the [exceedance_proc_state]. *)
   Variable sched : schedule (exceedance_proc_state Job).