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 8 minutes and 13 seconds (queued for 2 seconds)
merge request