proofs breaking in Std/Data/Array/Init/Lemmas.lean

Stream: batteries

[Kim Morrison]

Now that https://github.com/leanprover/lean4/pull/2295 has landed, two proofs in Std/Data/Array/Init/Lemmas.lean will break.

Just in case anyone (Mario?) is eager to fix these, the lean-toolchain semorrison/lean4:eece499 is available, which includes this fix. Otherwise it will land in the next nightly.

[Mario Carneiro]

I usually just wait for the nightly