case h.h
α : Type u_1
l : List α
⊢ inits l = initsTR l
⊢ @inits = @initsTR
funext α l
case h.h
α : Type u_1
l : List α
⊢ inits l = reverse (foldr (fun a arrs => Array.push (Array.map (fun t => a :: t) arrs) []) #[[]] l).data
case h.h
α : Type u_1
l : List α
⊢ inits l = initsTR l
simp [initsTR]
no goals
case h.h
α : Type u_1
l : List α
⊢ inits l = reverse (foldr (fun a arrs => Array.push (Array.map (fun t => a :: t) arrs) []) #[[]] l).data
induction l <;> simp [*, reverse_map]