1 NAMING CONVENTIONS FOR METAVARIABLES
4 F,G : subset of subterms
10 S : arbitrary small type
11 T, U, V, W: subset of subterms
16 d, e : variable reference level
18 i, j : variable reference depth (de Bruijn index)
21 m, n : measures on terms
23 r, s : pointer sequence