WIP
WIP
WIP
still have an incomplete proof
some clean up
I didn't need MyList, List will do, xInTail demonstrates possible need for the (-->) functor
WIP
WIP
cleaned up the proofs
WIP: Cleaning up proofs