Rocq Prover good first issues

This meta-issue outlines Jason's plan to extend McTT as a research platform. Key areas include handling local/global definitions and modules, refactoring explicit substitutions into an operation, and implementing contra-variant subtyping. These are presented in rough ascending order of difficulty, with the latter two items posing significant challenges.