This way we avoid the env_cbv tactic unfolding string related stuff
that appears in the goal and hypotheses of the proof mode.