[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