English
If f,g: α → β → β and b ∈ β and l ∈ List α satisfy ∀ a ∈ l, ∀ b, f a b = g a b, then foldr f b l = foldr g b l.
Русский
Если f,g: α → β → β и b, l удовлетворяют условию ∀ a ∈ l, ∀ b, f a b = g a b, тогда foldr f b l = foldr g b l.
LaTeX
$$$\\\\forall {f,g:\\\\alpha \\\\to \\\\beta \\\\to \\\\beta} {b:\\\\beta} {l:\\\\text{List }\\\\alpha},\\\\,\\\\forall a \\\\in l,\\\\,\\\\forall b:\\\\beta, f a b = g a b \\\\Rightarrow \\\\operatorname{foldr} f b l = \\\\operatorname{foldr} g b l.$$$
Lean4
theorem foldr_ext (f g : α → β → β) (b : β) {l : List α} (H : ∀ a ∈ l, ∀ b : β, f a b = g a b) :
foldr f b l = foldr g b l :=
by
induction l with
| nil => rfl
| cons hd tl ih => ?_
simp only [mem_cons, or_imp, forall_and, forall_eq] at H
simp only [foldr, ih H.2, H.1]
