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: Oct 12 2024 at 20:18 UTC