Another option allows searching for principal normal inhabitants. When pressing the "New Proof Tree" with the "Show Principality Cues" option, some edges and type-variables in the formula-tree appear colored.

This coloring might change during the construction of the proof-tree.

In order to construct principal normal inhabitants, after completion of
the proof-tree all edges and type-variables in the *formula-tree*
should be black. Then, all long terms in the corresponding set of
normal terms are principal (terms obtained by -reduction may
possibly be not principal). Conversely, if not all edges and
type-variables in the formula-tree are black after completion of a
proof-tree, then none of the corresponding terms is principal.

For changing colors the following rules apply:

- using a primitive part in the proof-tree turns all edges in this primitive part in the formula-tree black;
- overlapping occurrences of type-variables in the proof-tree receive the same color in the formula-tree (due to implementation, if all occurrences of a type-variable are have the same color, then they are all black).

So, if one chooses to use part

then the tail-variable in and the head-variable in receive the same color both in the proof-tree

as well as in the formula-tree and the edges in turn black.

Then, when completing the right branch with

the same happens to the occurrences of in and in :

Proceeding, one might construct the following proof-tree.

For this proof-tree all edges and type-variables in the formula-tree turned black:

This means that all *long* terms in the corresponding set of
normal terms are principal inhabitants.

Note, that terms in this set obtained by -reduction are not always principal inhabitants.