mathlib3

77168704 - feat(data/list/forall2): defines sublist_forall2 relation (#7165)

feat(data/list/forall2): defines sublist_forall2 relation (#7165) Defines the `sublist_forall₂` relation, indicating that one list is related by `forall₂` to a sublist of another. Provides two lemmas, `head_mem_self` and `mem_of_mem_tail`, which will be useful when proving Higman's Lemma about the `sublist_forall₂` relation. Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>