Module check
minitt
Type check: all about type checking.
genV in Mini-TT.
genV
upG in Mini-TT. Gamma |- p : t = u => Gamma’
upG