list.take_subset and simp

Stream: general

[Kevin Buzzard]

I can't find take n l ⊆ l for lists, so I was going to add it; I found @[simp] lemma subset_append_left (l₁ l₂ : list α) : l₁ ⊆ l₁++l₂ := ... in core, and I was surprised to see it was a simp lemma. Am I right in thinking that my lemma is missing? Should it be a simp lemma too?