Have `iFrame` smartly instantiate existentials
In the case the goal is e.g., of the form
P * ?Q, where
?Q is an existential, and we want to frame some assertion
R that does not appear, we may want to instantiate
R * ?Q'. Therefore, the meta-variable serves as a "buffer" where we put everything which we frame and fail to put anywhere else.
This is usefull in CFML, so I think I will implement this anyway in CFML. The reason it is usefull is that the typical CFML workflow implies working with an evar as a post-condition, which is instantiated by whatever is remaining.
Would you think this might be worth having in the general IPM?