lft is EqDecision and Countable

This adds EqDecision and Countable instances for lft to the lifetime logic's interface, analogously to the existing instances for atomic_lft.

These instances are used by RefinedRust (I overlooked them in my previous MR !38 (merged), and we only just noticed when porting to get rid of our fork of lambda-rust; sorry for the trouble!)

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