case h.h.h.h.h
α : Type u_2
β : Type u_1
f : α → β → β
init : β
l : List α
⊢ foldr f init l = foldrTR f init l
⊢ @foldr = @foldrTR
funext α β f init l
no goals
case h.h.h.h.h
α : Type u_2
β : Type u_1
f : α → β → β
init : β
l : List α
⊢ foldr f init l = foldrTR f init l
simp [foldrTR, Array.foldr_eq_foldr_data, -Array.size_toArray]