Various improvements to iFrame

This MR makes the following improvements to iFrame:

1. Framing under implications P → Q (since we already allowed framing under magic wands). This is possible if either the frame is persistent, or P is persistent.
2. Framing in both sides of a conjunction P ∧ Q (previously, it would frame in just one side). Concretely, framing in a conjunction will succeed if framing in either (or both) P or Q succeeds.
3. Stronger framing for disjunctions P ∨ Q Framing of a spatial frame will succeed if:

• Framing in both P and Q succeeds.
• Framing in P succeeds and turns it into True.
• Similarly for Q. Framing of a persistent frame will succeed if it succeeds in either (or both) P or Q.

Note that I previously objected to (3) in #145 (closed), however, I come back from that point. The example was artificial, and we already have plenty of situations where framing may lead to information loss. For example, try framing P in (False -∗ P) ∗ stuff.

This MR closes #145 (closed).