case nil
α : Type u
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type ?u.23411
μ : Type u_1
f : γ → δ → μ
g : α → γ
h : β → δ
bs : List β
⊢ zipWith f (map g []) (map h bs) = zipWith (fun a b => f (g a) (h b)) [] bs

case cons
α : Type u
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type ?u.23411
μ : Type u_1
f : γ → δ → μ
g : α → γ
h : β → δ
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (bs : List β), zipWith f (map g tail✝) (map h bs) = zipWith (fun a b => f (g a) (h b)) tail✝ bs
bs : List β
⊢ zipWith f (map g (head✝ :: tail✝)) (map h bs) = zipWith (fun a b => f (g a) (h b)) (head✝ :: tail✝) bs
α : Type u
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type ?u.23411
μ : Type u_1
f : γ → δ → μ
g : α → γ
h : β → δ
as : List α
bs : List β
⊢ zipWith f (map g as) (map h bs) = zipWith (fun a b => f (g a) (h b)) as bs
induction as generalizing bs
no goals
case nil
α : Type u
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type ?u.23411
μ : Type u_1
f : γ → δ → μ
g : α → γ
h : β → δ
bs : List β
⊢ zipWith f (map g []) (map h bs) = zipWith (fun a b => f (g a) (h b)) [] bs
simp
no goals
case cons
α : Type u
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type ?u.23411
μ : Type u_1
f : γ → δ → μ
g : α → γ
h : β → δ
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (bs : List β), zipWith f (map g tail✝) (map h bs) = zipWith (fun a b => f (g a) (h b)) tail✝ bs
bs : List β
⊢ zipWith f (map g (head✝ :: tail✝)) (map h bs) = zipWith (fun a b => f (g a) (h b)) (head✝ :: tail✝) bs
cases bs <;> simp [*]