`iRename` fails with bad error message when not in proof mode
Lemma silly : True. Proof. iRename "H" into "H".
Unable to unify "unseal environments.pre_envs_entails_aux ?PROP (environments.env_intuitionistic ?M11770) (environments.env_spatial ?M11770) ?M11775" with "True".
The tactic probably does not call
iStartProof at the beginning.