k : sort index
p,q : global reference position
t,u : local reference position level (de Bruijn's)
+x,y,z : reserved: transient objet denoted by a small letter
+
+NAMING CONVENTIONS FOR CONSTRUCTORS
+
+0: atomic
+2: binary
+
+A: application to vector
+
+a: application
+b: binder
+d: abbreviation
+f: flat
+l: abstraction
+t: native type annotation