(you can use "\" instead of "λ" and "^" instead of "∀")

Examples:
λX.λY.λZ.λx:XYZ.λy:XY.λz:X.xz(yz)
λX.λY.λZ.λx:XYZ.λy:XY.λz:X.(λu:Z.xzu)(yz)
λX.λf:XX.λx:X.f(fx)
λX.(λY.λf:YY.λx:Y.f(fx))(XX)((λY.λf:YY.λx:Y.f(fx))X)
λX.λx:X.x
λx:(∀X.XX).x(∀X.XX)x
(λx:(∀X.XX).x(∀X.XX)x)λX.λx:X.x
λx:(∀X.XX).x(∀X.XX)x(∀X.XX)x
(λx:(∀X.XX).x(∀X.XX)x(∀X.XX)x)λX.λx:X.x