p41. In Lemma 33, for C to preserve sorts, we need sorts to be irreducible by →.
p50. In Lemma 54, → needs to preserve typing in ⊢g.
p58. In Lemma 68, we assume the system to be logical and we do induction on ⊢ₛ.
