Inconsistent naming of list lemmas
Usually the lemmas defined in a "section" of the list files have that "section" as the first component of their name. That is not always the case though, e.g.
(** ** Properties of [subseteq] *)
Lemma list_delete_subseteq i l : delete i l ⊆ l.
Lemma list_filter_subseteq P `{!∀ x : A, Decision (P x)} l :
(** ** Properties of the [prefix] and [suffix] predicates *)
Lemma elem_of_prefix l1 l2 x :
x ∈ l1 → l1 `prefix_of` l2 → x ∈ l2.
So maybe they should be renamed? Though I think basically all elem_of
lemmas have that as their first component, so prefix_elem_of
would be somewhat strange...