Work in utils. Several more lemmas/ideas laid out.

Proving some fundamental statements about the Transitive Relation
Paths/lists (TPaths). Basically so they are very natural/convenient to
work with.

This should lead to tagging the ideas at the bottom of the file as
well, namely showing a list (TPath) built from a finite set has a
finite length, which can then be used with a reversed concept of a
TPath to show minimality of the partially ordered Nodes in a bundle.