case h.h.h
α : Type u_2
β : Type u_1
as : AssocList α β
⊢ toList as = toListTR as
⊢ @toList = @toListTR
funext α β as
case h.h.h
α : Type u_2
β : Type u_1
as : AssocList α β
⊢ toList as = (List.foldl (fun d x => Array.push d (x.fst, x.snd)) #[] (toList as)).data
case h.h.h
α : Type u_2
β : Type u_1
as : AssocList α β
⊢ toList as = toListTR as
simp [toListTR]
no goals
case h.h.h
α : Type u_2
β : Type u_1
as : AssocList α β
⊢ toList as = (List.foldl (fun d x => Array.push d (x.fst, x.snd)) #[] (toList as)).data
exact .symm <| (Array.foldl_data_eq_map (toList as) _ id).trans (List.map_id _)