NAMING CONVENTIONS FOR METAVARIABLES
A, B, C, D: term
+F,G : subset of subterms
H : transient premise
IH : inductive premise
M, N : term
+P, Q : pointer tree
R : arbitrary relation
-T, U : arbitrary small type
+S : arbitrary small type
+T, U, V, W: subset of subterms
-a, b : boolean
-d, e : variable reference depth
+a : arbitrary element
+b,c : boolean mark
+d, e : variable reference level
+f : arbitrary function
h : relocation height
-i, j : de Bruijn index
+i, j : variable reference depth (de Bruijn index)
k : relocation height
l : arbitrary list
m, n : measures on terms
-p, q : redex pointer
-r, s : redex pointer sequence
-t, u : arbitrary element
+o : pointer step
+p, q : pointer
+r, s : pointer sequence