move instances

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.

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 (⊓) := _.