--- /dev/null
+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
+S : arbitrary small type
+T, U, V, W: subset of subterms
+
+a : arbitrary element
+b,c : boolean mark
+d, e : variable reference level
+f : arbitrary function
+h : relocation height
+i, j : variable reference depth (de Bruijn index)
+k : relocation height
+l : arbitrary list
+m, n : measures on terms
+o : pointer step
+p, q : pointer
+r, s : pointer sequence