Strong induction on lists

Stream: Is there code for X?

[Marcus Rossel]

Does a theorem like the following already exists somewhere in some form?

-- Note: The induction hypothesis states "if l₂ is a strict suffix of hd::tl, then p l₂".
theorem List.strongInduction {p : List α → Prop} (l : List α)
    (nil  : p [])
    (cons : ∀ hd tl, (∀ {hd₁ tl₁ l₂}, hd₁::tl₁ ++ l₂ = hd::tl → p l₂) → p (hd::tl)) :
    p l := by
  generalize hl : l.length = len
  induction len using Nat.strongInductionOn generalizing l <;> cases ‹Nat› <;> cases l
  case ind.succ.cons hi _ _ => exact cons _ _ fun h => hi _ (by simp_arith [←hl, ←h]) _ rfl
  all_goals simp_all

If not, would it be viable to add this to mathlib?

[Shreyas Srinivas]

Maybe it is/should be in Std?