diff --git a/analysis/facts/preemption/rtc_threshold/floating.v b/analysis/facts/preemption/rtc_threshold/floating.v
index 5cb88383616dc618689f95d39fd427d663b6a2a9..53d2804df743787c42b76750d025cc92d8f01699 100644
--- a/analysis/facts/preemption/rtc_threshold/floating.v
+++ b/analysis/facts/preemption/rtc_threshold/floating.v
@@ -1,8 +1,5 @@
 Require Export prosa.analysis.facts.preemption.task.floating.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
-
-(** Furthermore, we assume the task model with floating non-preemptive regions. *)
-Require Import prosa.model.preemption.limited_preemptive.
 Require Import prosa.model.task.preemption.floating_nonpreemptive.
 
 (** * Task's Run to Completion Threshold *)
@@ -10,6 +7,9 @@ Require Import prosa.model.task.preemption.floating_nonpreemptive.
     threshold] for the model with floating non-preemptive regions. *)
 Section TaskRTCThresholdFloatingNonPreemptiveRegions.
 
+  (** Furthermore, we assume the task model with floating non-preemptive regions. *)
+  #[local] Existing Instance floating_preemptive.
+
   (** Consider any type of tasks ... *)
   Context {Task : TaskType}.
   Context `{TaskCost Task}.
diff --git a/model/task/preemption/floating_nonpreemptive.v b/model/task/preemption/floating_nonpreemptive.v
index b1c78d78685e1a67d40c9360ca70c23c89369832..60d621e7ff38869a5a5160ba6fa436a7ac281906 100644
--- a/model/task/preemption/floating_nonpreemptive.v
+++ b/model/task/preemption/floating_nonpreemptive.v
@@ -59,9 +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]. *)
-  Global Program Instance fully_preemptive : TaskRunToCompletionThreshold Task :=
-    {
-      task_rtct (tsk : Task) := task_cost tsk
-    }.
+  Definition floating_preemptive : TaskRunToCompletionThreshold Task :=
+    fun tsk : Task => task_cost tsk.
 
 End TaskRTCThresholdFloatingNonPreemptiveRegions.