1 NAMING CONVENTIONS FOR METAVARIABLES
4 C,D : candidate of reducibility
7 H : reserved: transient premise
8 IH : reserved: inductive premise
10 K,L : local environment
11 M,N : reserved: future use
13 P,Q : reserved: future use (lambda_delta 4)
14 R : generic predicate (relation)
17 X,Y,Z : reserved: transient objet denoted by a capital letter
19 a,b : reserved: future use (lambda_delta 4)
20 c : reserved: future use (lambda_delta 3)
24 g : sort degree parameter
25 h : sort hierarchy parameter
26 i,j : local reference position index (de Bruijn's)
29 m,n : reserved: future use
31 p,q : global reference position
33 t,u : local reference position level (de Bruijn's)
35 x,y,z : reserved: transient objet denoted by a small letter
37 NAMING CONVENTIONS FOR CONSTRUCTORS
42 A: application to vector
49 n: native type annotation