diff --git a/lifetime/lifetime_sig.v b/lifetime/lifetime_sig.v
index 095c95608cf7cacb10d1f610a4f2bfeceea6bf9d..451a072702ec9df4d95db5d451c338cd3b3ad760 100644
--- a/lifetime/lifetime_sig.v
+++ b/lifetime/lifetime_sig.v
@@ -67,7 +67,14 @@ Module Type lifetime_sig.
   Global Declare Instance lft_inhabited : Inhabited lft.
   Global Declare Instance lft_eq_dec : EqDecision lft.
   Global Declare Instance lft_countable : Countable lft.
+
+  Global Declare Instance atomic_lft_inhabited : Inhabited atomic_lft.
+  Global Declare Instance atomic_lft_eq_dec : EqDecision atomic_lft.
+  Global Declare Instance atomic_lft_countable : Countable atomic_lft.
+
   Global Declare Instance bor_idx_inhabited : Inhabited bor_idx.
+  Global Declare Instance bor_idx_eq_dec : EqDecision bor_idx.
+  Global Declare Instance bor_idx_countable : Countable bor_idx.
 
   Global Declare Instance lft_intersect_comm : Comm (A:=lft) eq (⊓).
   Global Declare Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓).
@@ -112,8 +119,6 @@ Module Type lifetime_sig.
   Global Declare Instance atomic_lft_to_lft_inj : Inj eq eq atomic_lft_to_lft.
   Global Declare Instance positive_to_atomic_lft_inj : Inj eq eq positive_to_atomic_lft.
 
-  Global Declare Instance atomic_lft_eq_dec : EqDecision atomic_lft.
-  Global Declare Instance atomic_lft_countable : Countable atomic_lft.
 
   (** * Laws *)
   Parameter lft_tok_sep : ∀ q κ1 κ2, q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
diff --git a/lifetime/model/definitions.v b/lifetime/model/definitions.v
index ee360cda76d68a07cd465190bc36e4435ba9b237..35fdc4a09faae5df40bac0cca1551ecc6962643f 100644
--- a/lifetime/model/definitions.v
+++ b/lifetime/model/definitions.v
@@ -353,6 +353,7 @@ Qed.
 Global Instance positive_to_atomic_lft_inj : Inj eq eq positive_to_atomic_lft.
 Proof. apply _. Qed.
 
+Global Definition atomic_lft_inhabited : Inhabited atomic_lft := _.
 Global Definition atomic_lft_eq_dec : EqDecision atomic_lft := _.
 Global Definition atomic_lft_countable : Countable atomic_lft := _.
 End basic_properties.
diff --git a/lifetime/model/primitive.v b/lifetime/model/primitive.v
index 4f32bf1148f58dd539561ef27ab5eb22ee8aaf9f..a9104e8f19a8c5eba7c872b4893a81af7ac612ee 100644
--- a/lifetime/model/primitive.v
+++ b/lifetime/model/primitive.v
@@ -306,6 +306,8 @@ 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 bor_idx_eq_dec : EqDecision bor_idx := _.
+Local Instance bor_idx_countable : Countable bor_idx := _.
 Local Instance lft_intersect_comm : Comm (A:=lft) eq (⊓) := _.
 Local Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓) := _.
 Local Instance lft_intersect_inj_1 κ : Inj eq eq (κ ⊓.) := _.