English
Let f: α → β → γ and p: γ → Prop. For lists l1 and l2 with certain length, Forall p (zipWith f l1 l2) is equivalent to Forall₂ (λ x y, p (f x y)) l1 l2.
Русский
Пусть f: α → β → γ и p: γ → Prop. При списках l1, l2 одинаковой длины выражение Forall p (zipWith f l1 l2) эквивалентно Forall₂ (λ x y, p (f x y)) l1 l2.
LaTeX
$$$\forall f\, p\, (l_1 : List α) (l_2 : List β),\ length l_1 = length l_2 \to\big(Forall p (zipWith f l_1 l_2) \iff Forall_2 (\\lambda x y, p (f x y)) l_1 l_2\big)$$$
Lean4
theorem forall_zipWith {f : α → β → γ} {p : γ → Prop} :
∀ {l₁ : List α} {l₂ : List β},
length l₁ = length l₂ → (Forall p (zipWith f l₁ l₂) ↔ Forall₂ (fun x y => p (f x y)) l₁ l₂)
| [], [], _ => by simp
| a :: l₁, b :: l₂, h => by
simp only [length_cons, succ_inj] at h
simp [forall_zipWith h]
