Smarter iFrame: Prefer framing below `*` over framing below disjunction or wand
When framing below a disjunction or a wand/implication, it can happen that
P could have been framed elsewhere, and that would have been smarter. This is the case both for
(True \/ P) * P and
(False -* P) * P.
One possible way to solve this would be to have some kind of precedence for "framing positions" and not stop searching just because we found one below a disjunction/wand.