d : term degree
e : reserved: future use (\lambda\delta 3)
f,g : local reference transforming map
h : sort hierarchy parameter
i,j : local reference depth (de Bruijn's)
k,l : global reference level
d : term degree
e : reserved: future use (\lambda\delta 3)
f,g : local reference transforming map
h : sort hierarchy parameter
i,j : local reference depth (de Bruijn's)
k,l : global reference level