GitLab

Hi!

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.