NAMING CONVENTIONS FOR METAVARIABLES

A,B    : arity
C,D    : candidate of reducibility
E,F,G  : reserved: future use
H      : reserved: transient premise
IH     : reserved: inductive premise
I,J    : item
K,L    : local environment
M,N    : reserved: future use
O      : reserved: standard library
P,Q    : reserved: future use
R      : generic predicate (relation)
S      : reserved: standard library
T,U,V,W: term
X,Y,Z  : reserved: transient objet denoted by a capital letter

d      : relocation depth
e      : relocation height
h      : sort hierarchy parameter
i,j    : local reference position index (de Bruijn's)
k      : sort index
p,q    : global reference position