Remove explicit substitutions

[HuStmpHrrr]

Currently, McTT uses explicit substitution calculus, only because Abel's habilitation thesis does so. In the thesis, the motivation of explicit substitutions is to simplify the proof by avoiding reasoning about the relation between substitutions and the evaluation of substitutions. Unfortunately, as we expand features in McTT, explicit substitutions have become an inviable option: explicit substitutions place originally definitional equations into syntactic equivalence, which in addition carries typing information. As a result, reasoning about explicit substitutions will become (or worse, is already) very cumbersome, as we include more and more features.

Therefore, it becomes essential to remove explicit substitutions for this project to work in a longer term.

We can use tools like autosubst to generate substitutions that compute. Now, the only difficulty left is to figure out how the model should work. I think morally, the following relation should hold in the PER model without explicit substitutions:

[[ t [ sigma ] ]] (rho) ~~ [[ t ]] ( [[ sigma ]] (rho) ） in [[ T ]]

for well-typed terms and substitutions. This leads to a change to the definitions of semantic typing for completeness. I think we need to include this condition into the definitions for it to work out. However, I don't have all the details right now. Let's put some thoughts into it and see how it is worked out eventually.

I think a helpful way forward is to experiment with simple types.