Write `wp_` lemmas for array operations in a more `iApply`/`wp_apply` friendly way

See this discussion: wp_apply only works poorly for array accesses currently due to Z vs nat conflicts. We should find a way to do better.

Equipping wp_load with support for array accesses is certainly a good idea, but I think we should also figure out a way to write such lemmas in a more apply-friendly style that can be used by other lemmas without having to write a tactic for each of them.