∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} {l₁ l₂ : List α},
  l₁.Perm l₂ →
    (∀ x ∈ l₁, ∀ y ∈ l₁, ∀ (z : β), f y (f x z) = f x (f y z)) →
      ∀ (init : β), List.foldr f init l₁ = List.foldr f init l₂