Connect the ott implementatin and the haskell implementation

I think a good way of doing this, is to refer to the ott identifiers instead of arbitrary or latex ones.

We should do this for:

• Datatypes
• Judgement headers

We already do this for the rules.

This requires us to refactor the ott implementation. We would also have to use new notation for ott identifiers that carry an index, and maybe even change the index metavariables. Example:

In ott, instead of using phi as the identifier for \phi, we use phy, because i is used as an index. We could easily use z instead and have it be typset as "i".

OTT: IDENT would be a good notation in my opinion.