no goals
α : Type u_1
β : Type ?u.248636
γ : Type ?u.248639
σ : Type ?u.248642
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
l : List α
⊢ (List.casesOn (id l) none fun b l_1 => some (l, b, l_1).snd.fst) = List.head? l
cases l <;> rfl