mathlib

b20e6647 - feat(order/well_founded_set): Higman's Lemma (#7212)

feat(order/well_founded_set): Higman's Lemma (#7212) Proves Higman's Lemma: if `r` is partially well-ordered on `s`, then `list.sublist_forall2` is partially well-ordered on the set of lists whose elements are in `s`.