TPath Lists <-> Transitive Closure. We can now use either.

- Main accomplishment: Proved that if two elements, x and y, are
related via the transitive closure of a relationship, then there is a
list that is the Transitive List Path of that relation (see
trans_imp_tpath).

The converse has also been proven. That if a transitive List Path
exists for the path x->y then they are related via transitive closure
as well (clos_trans X R x y).

This means we can go back and forth between the more natural transitive
closure, etc of related items and their transitive list.

- Other accomplishment: just tried to make names more clear, and
lemma/theorems' names more indicative of what they are about than
previously was the case.