and others added 30 commits
One proof is admitted; should be easy to fix :)
The new refinement added some low-cost hints that were messing up the statement of the theorem by resolving to the wrong refinement layer. It is now annotated so that it is stated about the base system, not any of the refinements.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters