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:
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.