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