lft is EqDecision and Countable

lifetime/lifetime_sig.v

@@ -65,6 +65,8 @@ Module Type lifetime_sig.
 
   (** * Instances *)
   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 bor_idx_inhabited : Inhabited bor_idx.
 
   Global Declare Instance lft_intersect_comm : Comm (A:=lft) eq (⊓).

lifetime/model/definitions.v

@@ -356,4 +356,7 @@ 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.