TheoWinterhalter
diff --git a/‎chapters/elim-rel.tex‎
Lines changed: 1 addition & 1 deletion b/‎chapters/elim-rel.tex‎
Lines changed: 1 addition & 1 deletion
@@ -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
Original file line number	Diff line number	Diff line change
`@@ -314,7 +314,7 @@ \section{Properties of the relation}`
`314`	`314`	`translation~\sidecite{bernardy2012proofs}.`
`315`	`315`	`%`
`316`	`316`	`Our fundamental lemma on the decoration relation $\sim$ assumes two`
`317`		`-related terms of potentially different types $T1$ and $T2$ to produce an`
	`317`	`+related terms of potentially different types $T_1$ and $T_2$ to produce an`
`318`	`318`	`heterogeneous equality between them. For induction to go through under`
`319`	`319`	`binders (e.g. for dependent products and abstractions), we hence need to`
`320`	`320`	`consider the two terms under different, but heterogeneously equal`