no goals
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
f : β₁ → β₂
g₁ : α → β₁ → β₁
g₂ : α → β₂ → β₂
l : List α
init : β₁
H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)
⊢ foldr g₂ (f init) l = f (foldr g₁ init l)
induction l <;> simp [*, H]