tac_specialize_assert_pure: do not assume that pure things are persistent

This improves our support for BIs without a persistence modality.
IntoWand needs to be made a bit smarter, but it seems to still work for the cases in the repo.
2 jobs for !799 with ralf/proofmode-emp in 6 minutes and 50 seconds (queued for 3 seconds)
merge request