Remove workaround.

This bug is strange:

- In order to type check the argument `I : gmap lft lft_names`, Coq needs an
  instance `Countable lft`. Since `finite.finite_countable` has been declared
  using `Hint Immediate` it will try that instance first (*), which means it
  has to find an instance `Finite lft`.
- Apparently, at this moment the type of the argument `A` has not been inferred
  by the type checker yet. So, there is a hypothesis `A : ?T`.
- In order to prove `Finite lft`, Coq unifies `?T` with `Finite lft` and uses
  the hypothesis `A`.
- Subsequent type checking fails, because `gmap lft lft_names` is type checked
  using a wrong/arbitrary instance `Countable lft`.

This is probably a Coq bug: type class search should not just unify with
hypotheses whose type is just an evar.

(*) `finite.finite_countable` has been declared using `Hint Immediate` to make
sure it is only used at leafs, not to make sure that it is used first.

theories/lifetime/model/creation.v

@@ -55,11 +55,7 @@ Proof.
   iModIntro. rewrite /lft_inv_dead. iExists Q. by iFrame.
 Qed.
 
-(* FIXME: Get rid of this hack.  If we just remove this line, the next lemma
-   statement breaks. *)
-Remove Hints finite.finite_countable : typeclass_instances.
-
-Lemma lfts_kill A (I : gmap lft lft_names) (K K' : gset lft) :
+Lemma lfts_kill (A : gmap atomic_lft _) (I : gmap lft lft_names) (K K' : gset lft) :
   let Iinv K' := (own_ilft_auth I ∗ [∗ set] κ' ∈ K', lft_inv_alive κ')%I in
   K ⊥ K' →
   (∀ κ κ', κ ∈ K → is_Some (I !! κ') → κ ⊆ κ' → κ' ∈ K) →