Update notations

[Ailrun]

This allows us to exploit the power of Coq notation to write an object expression closer to metal.
If one wants to write a judgement, they can use {{ and }} (double {}), and to write an object expression solely, they can use {{{ and }}} (triple {}).
Some of the inconsistent names are fixed as well during the refactoring.

@HuStmpHrrr and @Antoine-something: Please let me know if you have any questions/concerns about the notations.

[HuStmpHrrr]

I thought originally judgments can just be written without {{? What does this buy us?

[Ailrun]

By writing {{}}, we can write contexts/terms/types in a more friendly syntax. It is basically {{{ \Gamma }}} \vdash {{{ term... }}} : {{{ type... }}} with the previous judgement syntax.