Some utility functions/proofs in util.v -- IN PROGRESS

Some list boilerplate code that should make it more convenient/flexible
using lists to represent "paths," or the transitive closure of
relations.