work on depenent types.

- simplifying hlist_eta proofs.
- rename vector to tuple since it is implemented as a tuple.
- start real vectors.