Danil Annenkov

We probably need to use the same trick as here: https://github.com/MetaCoq/metacoq/blob/coq-8.11/test-suite/univ.v#L64, which relaces all names with `nAnon`.

I am in the process of uncommenting code in the test-suit for universes.

> It must not like numbers as identifiers. Oops, I forgot to post the full error: `Error: Invalid character '.' in identifier "MetaCoqPolymophicTest.155".` So the problem is the dot, which...

Hi guys, I think, n-ary application makes a big difference in convenience for reasoning. I believe that the `mkApps` smart constructor is used in various relations (and, IIRC, in substitution)...

Yes, good point. Actually, since I am translating to `term` from another type of expressions (with only binary applications), my translation guarantees that there are no empty or nested applications,...

I still struggle with my proof involving `mkApps`. I think, if I targeted PCUIC instead, my development would be much easier. So, the question is which Ast makes more sense...

> would the translation require that stacked (binary) tApp in PCUIC get translated to one big Template Coq tApp (taking a term and a list)? This is exactly the part...

Another thing that looks a bit strange to me: `mkApps` is also used in substitution (although, there might be a good reason for that). Because of this I didn't have...

@mattam82 were you asking me about the language I am translating? (I mean, Abhishek didn't comment on this issue). I am working of embedding of mini-ml style (plus inductives and...

I've ported parts of my development to target PCUIC, but it turns out I just pushed the issue with `mkApps` to another corner. Now inverting anything involving PCUICWcbvEval.eval relation is...