A,B : arity
C,D : candidate of reducibility
-E,F,G : reserved: future use
+E,F : RTM environment
+G : global environment
H : reserved: transient premise
IH : reserved: inductive premise
I,J : item
K,L : local environment
M,N : reserved: future use
-O : reserved: standard library
+O :
P,Q : reserved: future use
R : generic predicate (relation)
-S : reserved: standard library
+S : RTM stack
T,U,V,W: term
X,Y,Z : reserved: transient objet denoted by a capital letter
h : sort hierarchy parameter
i,j : local reference position index (de Bruijn's)
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