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 ?Q
with 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?