#Typed lambda terms#
-Given a set of types `T`, we define the set of typed lambda terms <code>&Lamda;_T</code>,
+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,