Stronger `list_core_id`
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.