This tweak allows us to declare pvs as an instance of FromPure (it is not
an instance of IntoPure), making some tactics (like iPureIntro and done)
work with pvs too.