Given a set of types `T`, we define the set of typed lambda terms <code>Λ_T</code>,
which is the smallest set such that
-* each type `t` has an infinite set of distinct variables, {x^t}_1,
- {x^t}_2, {x^t}_3, ...
+* each type `t` has an infinite set of distinct variables, x<sup>t</sup><sub>1</sub>,
+ x<sup>t</sup><sub>2</sub>, x<sup>t</sup><sub>3</sub>, ...
* If a term `M` has type σ -> τ, and a term `N` has type
σ, then the application `(M N)` has type τ.