More cleanup and better typing for proofs/lemmas

The plan here is to first do some additional cleanup and then fix the typing logic in proofs/make application of lemmas typed. The branch this is going to be implemented in is https://gitlab.imn.htwk-leipzig.de/waldmann/cyp/-/tree/73-cleanup-and-typing-lemmas

Cleanup:

• Use source span error messages where possible (https://gitlab.imn.htwk-leipzig.de/waldmann/cyp/-/issues/63)
• Replace the different typeDoc, kindDoc etc. functions, they aren't needed anymore and can be replaced by pretty
• Gradually adapt the old test-cases to the new system described in https://gitlab.imn.htwk-leipzig.de/waldmann/cyp/-/issues/49, while (probably?) making the negative test-cases more accepting, i.e. not having to match an expected output word for word. It is kind of annoying to have to fix the expected output of multiple tests when fixing error messages and creates a lot of work for some types of normally small changes. It is kind of useful to require negative tests to fail in a certain way, but matching expected output is not the best way to do this. A possible solution would be to have a different error datatype, that isn't just a Doc of the error message but for example has an associated error type. This could be realized by having something like data ErrorType = UnificationError | ProofValidationError | ... and then just checking that the error type generated by a negative test matches the expected error type. This would make changing error messages a lot easier, but seems like a somewhat big change. In the meantime, it's probably best to just not match negative tests against expected outputs.
• ...

Proofs/Lemmas:

• Right now in the typing for proofs, when we have a fixed variable "x~n", the index is just forgotten when typechecking and it is treated like a raw variable "x". There still isn't an issue with name clashes when typechecking, but it would be nicer to remember the index and maybe that makes it possible to make the typechecking easier in some places?
• It would probably be worth it to refactor Proof/Check.hs. Right now it is has this big checkProof-Function that does the following things for every proof type:
  • Validate the proofs parts, like induction variable, to show, etc.
  • Modify the environment. For example, in extensionality the extensionality variable is fixed via declareTerm, and the rest of the proof checking continues with this modified environment.
  • Check the proof.
• It would be nice to break up this big function into smaller ones, one for each proof type. Also, it might be good to incorporte proof typechecking right away, since we would also like to use the modified environment there? Else we have to replicate it, which would also be an option if we make the steps more modular.
• Application of lemmas should be typed! (https://gitlab.imn.htwk-leipzig.de/waldmann/cyp/-/issues/23)