add formal substitutions and deep memoization

[thibautbenjamin]

Ideas to improve the performance:

• Add formal substitutions to the unchecked syntax and to the kernel syntax. Instead of computing every term down to applied coherences, we could just have a syntax for applied term. The unchecked syntax should carry around checked terms to apply the same way it carries around checked coherences. typechecking of the checked terms should be much faster, as we only need to check the substitution, and that it matches the context of the term, using the cut rule. Checking term equality becomes more complex. If we are lucky, the two things are the same term applied to the same substitution. If it's not the case, we need to compute the terms down to coherences and checked that it's the same coherence applied to the same substitution. However, the comparison of substitution can now only be made by comparing locally maximal variables, because the substitutions are already checked, which gets around having to compute everything and should save a significant amount of time overall. Another benefit arises when constructing terms: it's not necessary anymore to compute applied substitutions everywhere but instead just store formal applications.

• Deep memoization: An idea due to Jamie, implemented in hotomotopy.io -> in the syntax tree, any two equal subterm should be physically the same, and every single operation should be memoized so that the same computation is never repeated twice. This seems harder to implement and I don't think it will have a big impact if we already implement the previous idea. But if even with the previous idea we are too slow we can try this.