Odomontois

The "only" lemma is because other lemmas are defined via \func

I've learned about \lemma and \property and HoTT precategories and univalent categories not so long ago. Now I'm planning to rewrite all of this from scratch

This repo was my first learning project. I barely knew Idris, and have no experience with HoTT. Please don't judge the language referring to this. You can refer nice code here https://github.com/JetBrains/arend-lib