`iDestruct 1` does not work when `Z_scope` is open
In this case, we have to write iDestruct 1%nat
. It would be perfect to add the tactic notation for Z, too.
In this case, we have to write iDestruct 1%nat
. It would be perfect to add the tactic notation for Z, too.