refactor: make `hIterate_elim` more specific

[alexkeizer]

Change the invariant Q to only have to be defined for Fin (w+1), rather than all Nats.

This is a strict generalization, and makes defining an invariant that doesn't necessarily make sense for arbitrary Nat a bit nicer (although it could be done before, using if h : i < w + 1 then ... else ...).