Hi all,

I have proved a fairly large theorem which has a large number of hypotheses. Is there a way (say using Ltac) that I can check if some hypotheses are unused in the final proof?

One way that comes to mind is to put all your hypotheses in a section using `Context`

. That way when you close the section, coq will not include unused hypotheses. Then you can clearly see using `About`

what the correct type for the theorem should be.

Last updated: Dec 06 2023 at 13:01 UTC