Pass on chap 13

chapters/elim-rel.tex

@@ -314,7 +314,7 @@ \section{Properties of the relation}
 translation~\sidecite{bernardy2012proofs}.
 %
 Our fundamental lemma on the decoration relation $\sim$ assumes two
-related terms of potentially different types $T1$ and $T2$ to produce an
+related terms of potentially different types $T_1$ and $T_2$ to produce an
 heterogeneous equality between them. For induction to go through under
 binders (e.g. for dependent products and abstractions), we hence need to
 consider the two terms under different, but heterogeneously equal