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

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