diff --git a/lifetime/model/definitions.v b/lifetime/model/definitions.v
index 900aad5046c1b8d27369b2df6f921f896a372406..ee360cda76d68a07cd465190bc36e4435ba9b237 100644
--- a/lifetime/model/definitions.v
+++ b/lifetime/model/definitions.v
@@ -355,8 +355,4 @@ Proof. apply _. Qed.
 
 Global Definition atomic_lft_eq_dec : EqDecision atomic_lft := _.
 Global Definition atomic_lft_countable : Countable atomic_lft := _.
-
-Global Definition lft_eq_dec : EqDecision lft := _.
-Global Definition lft_countable : Countable lft := _.
-
 End basic_properties.
diff --git a/lifetime/model/primitive.v b/lifetime/model/primitive.v
index 3fd9472c74ec87e79e86d38b8b0386a63be1ef1e..4f32bf1148f58dd539561ef27ab5eb22ee8aaf9f 100644
--- a/lifetime/model/primitive.v
+++ b/lifetime/model/primitive.v
@@ -303,6 +303,8 @@ Qed.
 
 (** Basic rules about lifetimes  *)
 Local Instance lft_inhabited : Inhabited lft := _.
+Local Instance lft_eq_dec : EqDecision lft := _.
+Local Instance lft_countable : Countable lft := _.
 Local Instance bor_idx_inhabited : Inhabited bor_idx := _.
 Local Instance lft_intersect_comm : Comm (A:=lft) eq (⊓) := _.
 Local Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓) := _.