feat: support for theorem disproof

[augustepoiroux]

This pull request introduces the ability to verify theorem disproofs. When allow_disproofs is set to true in config.json, one can solve a challenge by proving the negation of a theorem target instead of proving the theorem itself.

Key Changes

1. allow_disproofs: Added an optional config flag allow_disproofs (defaults to false).
2. Disproof Signature: Implemented signature matching in checkDisproof to verify that the disproof target (named <TheoremName>.disproof) is of type T → False or ¬ T.
3. Universe Matching: Support instantiating/matching universe level parameters to handle refutation of universe-polymorphic claims.

Design decisions to be discussed:

• What should happen when both foo and foo.disproof are submitted? In the current state, it prioritizes foo.disproof when present in the environment. Maybe a more sensible policy would be to accept a submission as long as one of foo and foo.disproof is correct.

Note: this PR is marked as a draft as it currently depends on leanprover/lean4export#36