truncation level of lists

[Alizter]

We add some more list functions and a proof that n.+2 truncated types give n.+2 truncated lists.

[jdchristensen]

Also, while it's unrelated to this PR, the list_pentagon result would fit better in Classes/implementations/list.v, right after app_assoc, as then this file wouldn't need to Require list.v.

[Alizter]

@jdchristensen I might do another cleanup after this where I move all the stuff in implmentations to Spaces so that we have all the list functions and lemmas in one place. What do you think?

[jdchristensen]

@jdchristensen I might do another cleanup after this where I move all the stuff in implmentations to Spaces so that we have all the list functions and lemmas in one place. What do you think?

Sounds fine. I guess that would mean that this file will still depend on some of the Classes library, then. Hmm, I just noticed that the existing list.v only needs canonical_names.v, not abstract_algebra.v, so that's a change that can also be made.

[Alizter]

I'm gonna remove the extra functions I added and leave that for the cleanup. I'll just keep the proof of the truncation level available here.

[jdchristensen]

LGTM.