Start implementing 'a vector.

metatheory works, but has 3 cheats. The inferencer has been updated, but
the proof doesn't build. The compiler and translator have not been
updated.

Surprisingly, so far most of the work has been because the fromList
primitive takes in a list, which is not itself a primitive type (it
starts in the initial environment instead). But future primitives that
involve lists (e.g., for arrays or strings) should also benefit from
this work.
Fix type soundness cheats.
Fix type inference proof
Update the values and do_app in the ILs

Truly horrible cut and pasting. I only see two ways around it:
- use a sed-like script to automatically generate each do_app function
  :(
- Include several different kinds of closures in the semantics' value
  type, and 3 different Conv constructors, basically putting the union
  of all IL values right up front. Then define predicates about which
  values can actually show up at any phase. This might be even worse
  than the status quo.
Update do_eq
modLang for vectors, but with 1 cheat.
More progress on vectors
modLangProof now cheat free
Merge remote-tracking branch 'origin/Word8Array' into alpha_vector
conLangProof down to one cheat

Which, alas, is not provable.
exhLangProof now cheat free
Remove a cheat
prove cheat in conLangProof
bit of progress on patLangProof
Merge remote-tracking branch 'origin/Word8Array' into alpha_vector

Conflicts:
	metatheory/typeSoundScript.sml
patLangProofs build with 4 cheats
add Vsub to impure operators

(because it can raise an exception)
prove one cheat in patLangProof
prove remaining cheats in patLangProof
update some do_app_cases theorems