Let `iRevert` of a pure hypotheses generate a wand instead of implication.

Because implications are strange and wands are nicer.

This matches with our general consensus to prefer wand/star over implication/conjunction.

In case the BI is not affine, the wand is weaker than the implication, so we add an affine modality.