C-c & C-v mostly (from strand.v basics). Defined ListWitness.

Ported over all the simple building blocks for strand spaces from
strand.v. This was primarily the basic definitions for terms and
messages, which will not change in this new real with more
constructive, tangible types and definitions.

Defined in util.v ListWitness which specifies a list of length 2 or
more where all adjacent members are related by some specified relation.
(Random note: where the heck are the pre-defined list annotations?
They're sitting in the List library in Coq but they weren't getting
imported… I couldn't find how to pull them in, so I copied the ones I
wanted, tweaked them slightly, and added 1. Whatever works.