When I call
Thm.hyps_of I get a list of open hypotheses of a theorem. Additionally, I may have a context that has the premises given by
Assumption.all_prems_of. Is there an efficient way to determine whether all hypotheses of the theorem are also premises of the context and can therefore considered to be closed (w.r.t the context)?
I think what I really need is to discharge those assumptions. Normally, the function
Assumption.export seems to be the right tool for the job. However, I only have one context so what is the target context? Just the global context?
Last updated: Dec 07 2023 at 16:21 UTC