simp? trace

Stream: mathlib4

[Johan Commelin]

In Data.List.Basic we had

theorem dropLast_cons_of_ne_nil {α : Type _} {x : α}
    {l : List α} (h : l ≠ []) : (x :: l).dropLast = x :: l.dropLast := by simp? [h]
-- Try this: simp only [_private.Std.Data.List.Init.Lemmas.0.List.dropLast._eq_3]

This seems to be a bug in simp?. The expected output is simp only [dropLast].