no goals
α : Type u_1
β : Type ?u.250075
γ : Type ?u.250078
σ : Type ?u.250081
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
l : List α
⊢ (List.casesOn (id l) [] fun b l_1 => (l, b, l_1).snd.snd) = List.tail l
cases l <;> rfl