1 NAMING CONVENTIONS FOR METAVARIABLES
4 C,D : candidate of reducibility
5 E,F,G : reserved: future use
6 H : reserved: transient premise
7 IH : reserved: inductive premise
9 K,L : local environment
10 M,N : reserved: future use
11 O : reserved: standard library
12 P,Q : reserved: future use
13 R : generic predicate (relation)
14 S : reserved: standard library
16 X,Y,Z : reserved: transient objet denoted by a capital letter
20 h : sort hierarchy parameter
21 i,j : local reference position index (de Bruijn's)
23 p,q : global reference position