more theory about lists

[Alizter]

This PR develops the theory of lists some more. Here is a summary of the changes:

• We change the [ a0; ...; an ] notation to [ a0, ..., an ] in a way that doesn't disrupt the pointed type notation.
• We add a new theories/Spaces/Option.v file for some basics about option types.
• In Option.v I needed to use the injection tactic which lets Coq prove that constructors of inductive types are injective. In order to do that, I had to register some constants in Overture.v. It appears to be working fine. See the proof of option_path.
• The head, nth and last functions now return an option A rather than requiring a default value.
• We add new functions:
  • drop which drops the first n elements of a list.
  • take which takes the first n elements of a list and returns it.
  • remove which removes the element at a given index.
  • nth' a variant of nth which takes a proof that the index is in bounds and guarantees an element.
  • repeat which repeats an element n times.
  • seq' a variant of seq which keeps around a proof that the elements are less than the length.
• We prove many new lemmas about the existing and new list functions and improve existing entries.
• We add comments to the Theory.v file.

These new functions and lemmas will be used in an upcoming PR.

[jdchristensen]

I skimmed some parts, but this looks good. Lots of results in this PR!

[jdchristensen]

I wonder if some of the results about nth' would be cleaner if first proved about nth and then converted to statements about nth' using nth_nth'? (Like how nth'_cons was done.)

[Alizter]

I tried nth'_map and I end up having to reason about nth returning Some when in range so it ended up not being shorter. I did not try nth'_map2 but presumably it has the same issue. That leaves only nth'_repeat and I would guess the nth_repeat proof would be the same length if we had it.