Show diff between expected and actual types in typechecking errors

[marat-rkh]

In Emacs mode for Coq, we can view the diff between expected and actual types in typechecking errors. This could be useful when types are large and it is not obvious which parts mismatch.

Example:

The diff:

We could add a similar feature for Arend.