In a situation like
H1: R H2: P ----------------------* R * (P /\ Q)
calling iFrame will turn the goal into
iFrame
----------------------* Q
This is too aggressive: Frequently, I will need P to prove Q.
P
Q
