diff --git a/analysis/facts/preemption/rtc_threshold/floating.v b/analysis/facts/preemption/rtc_threshold/floating.v
index 53d2804df743787c42b76750d025cc92d8f01699..b81a8101169fb68627ac5fea5bbb194246ee8426 100644
--- a/analysis/facts/preemption/rtc_threshold/floating.v
+++ b/analysis/facts/preemption/rtc_threshold/floating.v
@@ -8,7 +8,7 @@ Require Import prosa.model.task.preemption.floating_nonpreemptive.
 Section TaskRTCThresholdFloatingNonPreemptiveRegions.
 
   (** Furthermore, we assume the task model with floating non-preemptive regions. *)
-  #[local] Existing Instance floating_preemptive.
+  #[local] Existing Instance floating_preemptive_rtc_threshold.
 
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
diff --git a/analysis/facts/preemption/rtc_threshold/limited.v b/analysis/facts/preemption/rtc_threshold/limited.v
index 36f5e40f327559825c66c644f599beb590b24f85..54da3f195bf8c2c4cb1fb8c11e16db35694e2c22 100644
--- a/analysis/facts/preemption/rtc_threshold/limited.v
+++ b/analysis/facts/preemption/rtc_threshold/limited.v
@@ -12,7 +12,7 @@ Require Import prosa.model.preemption.limited_preemptive.
 Section TaskRTCThresholdLimitedPreemptions.
 
   (** We assume the task model with fixed preemption points. *)
-  #[local] Existing Instance limited_preemptions.
+  #[local] Existing Instance limited_preemptions_rtc_threshold.
 
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
@@ -104,7 +104,7 @@ Section TaskRTCThresholdLimitedPreemptions.
     split; first by rewrite /task_rtc_bounded_by_cost leq_subr.
     intros ? ARR__j TSK__j. move: (H_valid_fixed_preemption_points_model) => [LJ LT].
     move: (LJ) (LT) => [ZERO__job [COST__job SORT__job]] [ZERO__task [COST__task [SORT__task [T4 [T5 T6]]]]].
-    rewrite /job_rtct /task_rtct /limited_preemptions
+    rewrite /job_rtct /task_rtct /limited_preemptions_rtc_threshold
             /job_last_nonpreemptive_segment /task_last_nonpr_segment /lengths_of_segments.
     case: (posnP (job_cost j)) => [Z|POS]; first by rewrite Z; compute.
     have J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
diff --git a/analysis/facts/preemption/rtc_threshold/nonpreemptive.v b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
index ce67a5b82fcddf9d7c46b0e0183a65af8d63438d..0982fbacc79a844387ce81e124c157a94ac2a915 100644
--- a/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
@@ -9,9 +9,9 @@ Require Import prosa.model.task.preemption.fully_nonpreemptive.
 Section TaskRTCThresholdFullyNonPreemptive.
 
   (** We assume the fully non-preemptive task model. *)
-  #[local] Existing Instance fully_nonpreemptive_model.
-  #[local] Existing Instance fully_nonpreemptive.
-
+  #[local] Existing Instance fully_nonpreemptive_task_model.
+  #[local] Existing Instance fully_nonpreemptive_rtc_threshold.
+  
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}. 
   Context `{TaskCost Task}.
@@ -72,7 +72,7 @@ Section TaskRTCThresholdFullyNonPreemptive.
     intros; split.
     - by unfold task_rtc_bounded_by_cost.
     - intros j ARR TSK.
-      move: TSK => /eqP <-; rewrite /fully_nonpreemptive.
+      move: TSK => /eqP <-; rewrite /fully_nonpreemptive_rtc_threshold.
       edestruct (posnP (job_cost j)) as [ZERO|POS].
       + by rewrite job_rtc_threshold_is_0.
       + by erewrite job_rtc_threshold_is_ε; eauto 2. 
diff --git a/analysis/facts/preemption/rtc_threshold/preemptive.v b/analysis/facts/preemption/rtc_threshold/preemptive.v
index d8cbbeb4c4cb1afaaeff35c3e7079fe4fb480d39..04ad48fffcf5301b25d025e94ba5d8f980ca077a 100644
--- a/analysis/facts/preemption/rtc_threshold/preemptive.v
+++ b/analysis/facts/preemption/rtc_threshold/preemptive.v
@@ -12,8 +12,8 @@ Section TaskRTCThresholdFullyPreemptiveModel.
   (** We assume that jobs and tasks are fully preemptive. *)
   #[local] Existing Instance
     model.preemption.fully_preemptive.fully_preemptive_model.
-  #[local] Existing Instance fully_preemptive_model.
-  #[local] Existing Instance fully_preemptive.
+  #[local] Existing Instance fully_preemptive_task_model.
+  #[local] Existing Instance fully_preemptive_rtc_threshold.
 
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
diff --git a/analysis/facts/preemption/task/nonpreemptive.v b/analysis/facts/preemption/task/nonpreemptive.v
index 810081e5569d38a12cd4085bff7bb3ebd574e13d..1e9a62ee85e86c5fd8b3b3f1183cc5c7869bd358 100644
--- a/analysis/facts/preemption/task/nonpreemptive.v
+++ b/analysis/facts/preemption/task/nonpreemptive.v
@@ -10,8 +10,8 @@ Require Import prosa.model.task.preemption.fully_nonpreemptive.
 Section FullyNonPreemptiveModel.
 
   (** We assume the fully non-preemptive task model. *)
-  #[local] Existing Instance fully_nonpreemptive_model.
-  #[local] Existing Instance fully_nonpreemptive.
+  #[local] Existing Instance fully_nonpreemptive_task_model.
+  #[local] Existing Instance fully_nonpreemptive_rtc_threshold.
 
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
diff --git a/analysis/facts/preemption/task/preemptive.v b/analysis/facts/preemption/task/preemptive.v
index c5a8f4bf8c0ea443c7aae415df761fb21dcedd01..5dd416eb1b79787d3073f18d75b9c5cd78cf2f35 100644
--- a/analysis/facts/preemption/task/preemptive.v
+++ b/analysis/facts/preemption/task/preemptive.v
@@ -12,8 +12,8 @@ Section FullyPreemptiveModel.
   (** We assume that jobs and tasks are fully preemptive. *)
   #[local] Existing Instance
     model.preemption.fully_preemptive.fully_preemptive_model.
-  #[local] Existing Instance fully_preemptive_model.
-  #[local] Existing Instance fully_preemptive.
+  #[local] Existing Instance fully_preemptive_task_model.
+  #[local] Existing Instance fully_preemptive_rtc_threshold.
 
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
diff --git a/model/task/preemption/floating_nonpreemptive.v b/model/task/preemption/floating_nonpreemptive.v
index 60d621e7ff38869a5a5160ba6fa436a7ac281906..c15a8cdd6efce657889544ed586ee07250c36c73 100644
--- a/model/task/preemption/floating_nonpreemptive.v
+++ b/model/task/preemption/floating_nonpreemptive.v
@@ -59,7 +59,7 @@ Section TaskRTCThresholdFloatingNonPreemptiveRegions.
       information about the placement of preemption points in all jobs, i.e.,
       it is impossible to predict when exactly a job will be preemptable. Thus,
       the only safe run-to-completion threshold is [task cost]. *)
-  Definition floating_preemptive : TaskRunToCompletionThreshold Task :=
+  Definition floating_preemptive_rtc_threshold : TaskRunToCompletionThreshold Task :=
     fun tsk : Task => task_cost tsk.
 
 End TaskRTCThresholdFloatingNonPreemptiveRegions.
diff --git a/model/task/preemption/fully_nonpreemptive.v b/model/task/preemption/fully_nonpreemptive.v
index ca541512cf84aeef87eabfd1df8243bf556e7dbf..249dc0685d13feab0385023eb056c5ab956730dc 100644
--- a/model/task/preemption/fully_nonpreemptive.v
+++ b/model/task/preemption/fully_nonpreemptive.v
@@ -13,7 +13,7 @@ Section FullyNonPreemptiveModel.
   (** In the fully non-preemptive model, no job can be preempted until its
       completion. The maximal non-preemptive segment of a job [j] has length
       [job_cost j], which is bounded by [task_cost tsk].*)
-  Definition fully_nonpreemptive_model : TaskMaxNonpreemptiveSegment Task :=
+  Definition fully_nonpreemptive_task_model : TaskMaxNonpreemptiveSegment Task :=
     fun tsk : Task => task_cost tsk.
 
 End FullyNonPreemptiveModel.
@@ -31,7 +31,7 @@ Section TaskRTCThresholdFullyNonPreemptive.
       completion. In other words, once a job starts running, it is guaranteed
       to finish. Thus, we can set the task-level run-to-completion threshold
       to ε. *)
-  Definition fully_nonpreemptive : TaskRunToCompletionThreshold Task :=
+  Definition fully_nonpreemptive_rtc_threshold : TaskRunToCompletionThreshold Task :=
     fun tsk : Task => ε.
 
 End TaskRTCThresholdFullyNonPreemptive.
diff --git a/model/task/preemption/fully_preemptive.v b/model/task/preemption/fully_preemptive.v
index a6eea128852ea6419527798567a477613fc28915..f3d48b5fe4280da104e5b59ed31d1618d98e9bb4 100644
--- a/model/task/preemption/fully_preemptive.v
+++ b/model/task/preemption/fully_preemptive.v
@@ -13,7 +13,7 @@ Section FullyPreemptiveModel.
   (** In the fully preemptive model, any job can be preempted at any
       time. Thus, the maximal non-preemptive segment has length at most ε
       (i.e., one time unit such as a processor cycle). *)
-  Definition fully_preemptive_model : TaskMaxNonpreemptiveSegment Task :=
+  Definition fully_preemptive_task_model : TaskMaxNonpreemptiveSegment Task :=
     fun tsk : Task => ε.
 
 End FullyPreemptiveModel.
@@ -32,7 +32,7 @@ Section TaskRTCThresholdFullyPreemptiveModel.
   (** In the fully preemptive model, any job can be preempted at any
       time. Thus, the only safe run-to-completion threshold for a task
       is its WCET. *)
-  Definition fully_preemptive : TaskRunToCompletionThreshold Task :=
+  Definition fully_preemptive_rtc_threshold : TaskRunToCompletionThreshold Task :=
     fun tsk : Task => task_cost tsk.
 
 End TaskRTCThresholdFullyPreemptiveModel.
diff --git a/model/task/preemption/limited_preemptive.v b/model/task/preemption/limited_preemptive.v
index b0719ed112968de709427ed245e732dbd77af49e..c8e4d3b3903a5620f24889a7eb88dae4c78eac91 100644
--- a/model/task/preemption/limited_preemptive.v
+++ b/model/task/preemption/limited_preemptive.v
@@ -106,7 +106,7 @@ Section TaskRTCThresholdLimitedPreemptions.
       reaches its last non-preemptive segment. Thus, we can set the task-level
       run-to-completion threshold to [task_cost tsk - (task_last_nonpr_seg tsk - ε)],
       which safely bounds [job_cost j - (job_last_nonpr_seg j - ε)]. *)
-  Definition limited_preemptions : TaskRunToCompletionThreshold Task :=
+  Definition limited_preemptions_rtc_threshold : TaskRunToCompletionThreshold Task :=
     fun tsk : Task => task_cost tsk - (task_last_nonpr_segment tsk - ε).
 
 End TaskRTCThresholdLimitedPreemptions.
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index dcf9f74c192426212afeba4e3646cee712a9e034..79ed6a0fec44cce53ca432b24042b2d6fcfbcede 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -25,8 +25,8 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
   (** We assume that jobs and tasks are fully preemptive. *)
   #[local] Existing Instance
     model.preemption.fully_preemptive.fully_preemptive_model.
-  #[local] Existing Instance fully_preemptive_model.
-  #[local] Existing Instance fully_preemptive.
+  #[local] Existing Instance fully_preemptive_task_model.
+  #[local] Existing Instance fully_preemptive_rtc_threshold.
 
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
@@ -133,7 +133,7 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
   Proof.
     have BLOCK: blocking_bound  ts tsk = 0.
     { by rewrite /blocking_bound /parameters.task_max_nonpreemptive_segment
-                 /fully_preemptive.fully_preemptive_model subnn big1_eq. } 
+                 /fully_preemptive_task_model subnn big1_eq. } 
     try ( eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L) ) ||
     eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L := L) .
     all: rt_eauto.
diff --git a/results/fixed_priority/rta/fully_preemptive.v b/results/fixed_priority/rta/fully_preemptive.v
index 96df767026fb0d13acdda01e851e7babb4740ff1..f061dfadb3a31a916b8fb172fde7a2f195ddb35b 100644
--- a/results/fixed_priority/rta/fully_preemptive.v
+++ b/results/fixed_priority/rta/fully_preemptive.v
@@ -23,8 +23,8 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
   (** We assume that jobs and tasks are fully preemptive. *)
   #[local] Existing Instance
     model.preemption.fully_preemptive.fully_preemptive_model.
-  #[local] Existing Instance fully_preemptive_model.
-  #[local] Existing Instance fully_preemptive.
+  #[local] Existing Instance fully_preemptive_task_model.
+  #[local] Existing Instance fully_preemptive_rtc_threshold.
 
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
@@ -139,7 +139,7 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
   Proof.
     have BLOCK: blocking_bound ts tsk = 0.
     { by rewrite /blocking_bound /parameters.task_max_nonpreemptive_segment
-               /fully_preemptive.fully_preemptive_model subnn big1_eq. } 
+               /fully_preemptive_task_model subnn big1_eq. } 
     eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments.      
     all: rt_eauto.
     rewrite /work_bearing_readiness.