I needed a stronger version of
list_core_id that could depend on the structure of a particular list, similarly to
pair_core_id. I came up with this:
Global Instance list_core_id l : (forall x, x ∈ l -> CoreId x) -> CoreId l. Proof. intros Hyp. constructor. apply list_equiv_lookup=> i. rewrite list_lookup_core. destruct (l !! i) eqn:E. 2: done. apply Hyp. eapply elem_of_list_lookup; by eauto. Qed.
It probably could serve as a drop-in replacement for the old one.