case nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.89176
ε : Type ?u.89179
f g : α → β → γ
la : List α
lb : List β
⊢ zipWith f [] [] = zipWith g [] []

case cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.89176
ε : Type ?u.89179
f g : α → β → γ
la : List α
lb : List β
a : α
b : β
as : List α
bs : List β
hfg : f a b = g a b
a✝ : Forall₂ (fun a b => f a b = g a b) as bs
ih : zipWith f as bs = zipWith g as bs
⊢ zipWith f (a :: as) (b :: bs) = zipWith g (a :: as) (b :: bs)
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.89176
ε : Type ?u.89179
f g : α → β → γ
la : List α
lb : List β
h : Forall₂ (fun a b => f a b = g a b) la lb
⊢ zipWith f la lb = zipWith g la lb
induction' h with a b as bs hfg _ ih
no goals
case nil
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.89176
ε : Type ?u.89179
f g : α → β → γ
la : List α
lb : List β
⊢ zipWith f [] [] = zipWith g [] []
rfl
no goals
case cons
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.89176
ε : Type ?u.89179
f g : α → β → γ
la : List α
lb : List β
a : α
b : β
as : List α
bs : List β
hfg : f a b = g a b
a✝ : Forall₂ (fun a b => f a b = g a b) as bs
ih : zipWith f as bs = zipWith g as bs
⊢ zipWith f (a :: as) (b :: bs) = zipWith g (a :: as) (b :: bs)
exact congr_arg₂ _ hfg ih