NAMING CONVENTIONS FOR METAVARIABLES

A, B, C, D: term
H         : transient premise
IH        : inductive premise
M, N      : term
P, Q      : pointer tree
R         : arbitrary relation
T, U      : arbitrary small type

c         : pointer step
d, e      : variable reference level
h         : relocation height
i, j      : variable reference depth (de Bruijn index)
k         : relocation height
l         : arbitrary list
m, n      : measures on terms
p, q      : pointer
r, s      : pointer sequence
t, u      : arbitrary element