proofmode: do not treat pure assertions as persistent

Pure things being persistent requires bi_persistently_emp and excludes BIs without a persistence modality.

For iSpecialize, this means we now more often use IntoWand with the premise not being intuitionistic. This required tweaking our IntoWand instances for implication, but as far as I know those were previously rather ad-hoc. The most common usecase of implications is "P → ..." where Absorbing P (just like when we write P ∧ ..., usually P is absorbing), so that is what I evaluated the instances against:

• The existing into_wand_impl_true_false was rather odd in that it required the antecedent to be affine -- but P being both affine and absorbing will not happen. (We often write <affine> P -∗ ..., but never <affine> P → ....) The new into_wand_impl_true_false instead adds an affine modality around P, basically equivalent to if the user had written <affine> P -∗ ... instead.
• The existing into_wand_impl_false_false barely ever applies since it requires the implication itself to be absorbing. I removed that, instead requiring the antecedent to be persistent and absorbing, and adding an <affine> modality in front of it like the previous case.

I think the new instances make a lot more sense than the old ones; in particular, note how the into_wand_impl_false_false instance makes the "most" assumptions, and all the others (where some things are intuitionistic) just drop some of the requirements.