These tactics are superfluous:
- iPure H as pat => iDestruct H as pat
- iPersistent H => iSpecialize H "!"