First note, by analysis of the algorithm 2.6, that given a valid proof-tree , one has only if at least one primitive part has been used more than once in a branch of the proof-tree.

Now, consider the following definitions:

- occurs positively in ;
- if an occurrence of a subtype is positive (negative) in , then it is negative (resp. positive) in ;
- if an occurrence of a subtype is positive (negative) in , then it is positive (resp. negative) in .

On the other hand, it is easy to see by inspection of the
algorithm 2.3, that every negative (resp. positive) occurrence of
a type-variable in a type
appears as a
head-variable (resp. tail-variable) of a primitive part in the formula-tree.

Thus it is easy to conclude the following result by [1].