case nil
ι : Type ?u.229572
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : α → β → β
b : β
l : List α
H✝ : ∀ (a : α), a ∈ l → ∀ (b : β), f a b = g a b
H : ∀ (a : α), a ∈ [] → ∀ (b : β), f a b = g a b
⊢ foldr f b [] = foldr g b []

case cons
ι : Type ?u.229572
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : α → β → β
b : β
l : List α
H✝ : ∀ (a : α), a ∈ l → ∀ (b : β), f a b = g a b
hd : α
tl : List α
ih : (∀ (a : α), a ∈ tl → ∀ (b : β), f a b = g a b) → foldr f b tl = foldr g b tl
H : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), f a b = g a b
⊢ foldr f b (hd :: tl) = foldr g b (hd :: tl)
ι : Type ?u.229572
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : α → β → β
b : β
l : List α
H : ∀ (a : α), a ∈ l → ∀ (b : β), f a b = g a b
⊢ foldr f b l = foldr g b l
induction' l with hd tl ih
case cons
ι : Type ?u.229572
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : α → β → β
b : β
l : List α
H✝ : ∀ (a : α), a ∈ l → ∀ (b : β), f a b = g a b
hd : α
tl : List α
ih : (∀ (a : α), a ∈ tl → ∀ (b : β), f a b = g a b) → foldr f b tl = foldr g b tl
H : (∀ (b : β), f hd b = g hd b) ∧ ∀ (x : α), x ∈ tl → ∀ (b : β), f x b = g x b
⊢ foldr f b (hd :: tl) = foldr g b (hd :: tl)
case cons
ι : Type ?u.229572
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : α → β → β
b : β
l : List α
H✝ : ∀ (a : α), a ∈ l → ∀ (b : β), f a b = g a b
hd : α
tl : List α
ih : (∀ (a : α), a ∈ tl → ∀ (b : β), f a b = g a b) → foldr f b tl = foldr g b tl
H : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), f a b = g a b
⊢ foldr f b (hd :: tl) = foldr g b (hd :: tl)
simp only [mem_cons, or_imp, forall_and, forall_eq] at H
no goals
case cons
ι : Type ?u.229572
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : α → β → β
b : β
l : List α
H✝ : ∀ (a : α), a ∈ l → ∀ (b : β), f a b = g a b
hd : α
tl : List α
ih : (∀ (a : α), a ∈ tl → ∀ (b : β), f a b = g a b) → foldr f b tl = foldr g b tl
H : (∀ (b : β), f hd b = g hd b) ∧ ∀ (x : α), x ∈ tl → ∀ (b : β), f x b = g x b
⊢ foldr f b (hd :: tl) = foldr g b (hd :: tl)
simp only [foldr, ih H.2, H.1]
no goals
case nil
ι : Type ?u.229572
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f g : α → β → β
b : β
l : List α
H✝ : ∀ (a : α), a ∈ l → ∀ (b : β), f a b = g a b
H : ∀ (a : α), a ∈ [] → ∀ (b : β), f a b = g a b
⊢ foldr f b [] = foldr g b []
rfl