ι : Type ?u.144626
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β → γ
a : α
as : List α
b : β
bs : List β
⊢ flip f b a = f a b
ι : Type ?u.144626
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β → γ
a : α
as : List α
b : β
bs : List β
⊢ zipWith (flip f) (b :: bs) (a :: as) = zipWith f (a :: as) (b :: bs)
simp! [zipWith_flip]
no goals
ι : Type ?u.144626
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β → γ
a : α
as : List α
b : β
bs : List β
⊢ flip f b a = f a b
rfl