Improve framing below modalities

This MR improves framing below modalities:

1. It makes it possible to frame below an <affine> modality if the hypothesis that's framed is affine. (Previously, framing below <affine> was only possible if the hypothesis that's framed resides in the intuitionistic context.)
2. It will "clean up" redundant modalities among the "spine" of the frame.

Feature (2) is achieved by making the classes MakeAffinely, MakeIntuitionistically, MakeAbsorbingly, and MakePersistently "smarter". These classes already had ad-hoc "clean up" instances to avoid wrapping the input into a modality if that is not needed. For example, MakeAffinely would not wrap input P in an <affine> modality if P is affine, and would not turn input True into <affine> True, but instead turn True into emp.

This MR simply adds all combinations of "clean up" instances that I could think of. Namely:

• MakeAffinely True emp
• new MakeAffinely (<pers> P) (□ P)
• new MakeAffinely (<absorb> P1) P2 if BiPositive PROP and MakeAffinely P1 P2
• MakeAffinely P P if Affine P
• generalized MakeIntuitionistically P1 P2 if Persistent P1 and MakeAffinely P1 P2 (In particular, this instance maps input <pers> P to output □ P.)
• MakeAbsorbingly emp True
• new MakeAbsorbingly (<affine> P1) P2 if Persistent P1 and MakeAbsorbingly P1 P2
• new MakeAbsorbingly P P if Absorbing P
• new MakeAbsorbingly (□ P) (<pers> P)
• MakePersistently emp True
• new MakePersistently P1 P2 if Persistent P1 and MakeAbsorbingly P1 P2 (In particular, this instance maps input □ P to output <pers> P.)

I am not sure how useful this kind of "clean up" is in practice (it is only relevant for non-affine BIs anyway), but at least it now covers all combinations that I can think of instead of just some ad-hoc combinations as was done before. I have included a number of test cases to exercise this "clean up" as part of the iFrame tactic.

Moreover, as as a consequence of MakePersistently no longer creating redundant modalities, it can now be used to implement an alternative to the adhoc combination of FromPersistent and IntoAbsorbingly in !216 (closed). Concretely, similar to !216 (closed), this MR ensures that when using the [#] pattern on a premise that is not persistent, it will wrap the goal (using MakePersistently) into a <pers> modality (specialization would fail before). If the premise is already persistent, but not absorbing, it will add an absorbing modality (as was done before).