Proof-trees are tree-like structures and in the following we shall use the notation to designate a proof-tree with a variable at some leaf. Now, consider a type and let be the set of primitive parts in the formula-tree of , where is the primitive part in the root of (thus the only primitive part of form (P1) in ). Then, the set of proof-trees for is given by the following:

- If , then is a proof-tree for ;
- if is a proof-tree for and , where , then is a proof-tree for ;
- if is a proof-tree for and , then is a proof-tree for .

- all leaves in are of form (P3), i.e. no branch in ends with a variable;
- if , with is a primitive part in the formula-tree , and is a direct descendent/child of at branch , with , then above every occurrence of in there is at least one occurrence of in , such that the occurrence occurs in the subtree of rooted in the 'th branch of .

This last item corresponds to the hierarchy of
being imposed on the construction of a valid proof-tree.