no goals
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.6286
ε : Type ?u.6289
f : α → β → γ
p : γ → Prop
x✝ : length [] = length []
⊢ All₂ p (zipWith f [] []) ↔ Forall₂ (fun x y => p (f x y)) [] []
simp
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.6286
ε : Type ?u.6289
f : α → β → γ
p : γ → Prop
a : α
l₁ : List α
b : β
l₂ : List β
h : length l₁ = length l₂
⊢ All₂ p (zipWith f (a :: l₁) (b :: l₂)) ↔ Forall₂ (fun x y => p (f x y)) (a :: l₁) (b :: l₂)
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.6286
ε : Type ?u.6289
f : α → β → γ
p : γ → Prop
a : α
l₁ : List α
b : β
l₂ : List β
h : length (a :: l₁) = length (b :: l₂)
⊢ All₂ p (zipWith f (a :: l₁) (b :: l₂)) ↔ Forall₂ (fun x y => p (f x y)) (a :: l₁) (b :: l₂)
simp only [length_cons, succ_inj'] at h
no goals
α : Type u
β : Type u_1
γ : Type u_2
δ : Type ?u.6286
ε : Type ?u.6289
f : α → β → γ
p : γ → Prop
a : α
l₁ : List α
b : β
l₂ : List β
h : length l₁ = length l₂
⊢ All₂ p (zipWith f (a :: l₁) (b :: l₂)) ↔ Forall₂ (fun x y => p (f x y)) (a :: l₁) (b :: l₂)
simp [all₂_zipWith h]