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