C
T
T
CTT
Typechecking
Elimination
Equality
Synthesis