∀ {α : Type u_1} {β : Type u_2} {as bs : Array α},
  as = bs →
    ∀ {f g : β → α → β},
      f = g →
        ∀ {a b : β},
          a = b →
            ∀ {start start' stop stop' : ℕ},
              start = start' → stop = stop' → Array.foldl f a as start stop = Array.foldl g b bs start' stop'