Comment by JoeCamel

I'm a beginner in proof assistents, can you give some examples of many kinds of math ruled out? And what is UIP?