GitLab

In a situation like

H1: R
H2: P
----------------------*
R * (P /\ Q)

calling iFrame will turn the goal into

----------------------*
Q

This is too aggressive: Frequently, I will need P to prove Q.