Support primitive array terms

[mattam82]

This carries around primitive arrays down the MetaCoq pipeline. I tried to impact as little as possible the derivations, by using nested inductive types for auxiliary judgements. We now have a typing judgement for primitive arrays (modelled as lists, as array not nestable), and they get erased to just a default value and list of elements. In pcuic and erasure we use a bunch of generic lemmas for automating the proofs on the prim_val container, which works pretty well. We have reduction on arrays but they are not considered in evaluation yet, this will be the subject of a later PR. Interesting points:

• We prove no-confusion lemmas for conversion between applied axioms (i.e. primitive types) and products/inductives etc, to show correctness of erasure.
• We have generalized primitives so that they can carry terms, so we have to make substitution/lifting/reduction etc go through these which takes up a good part of the development (three more reduction rules to consider in confluence).
• Typechecking and erasure are rather straightforward otherwise.

[yforster]

ping @ed-hermoreyes (is Mireia also on github?), maybe file your changes introducing explicit admits as a PR against the primitive-arrays branch?

[JasonGross]

@mattam82 is there some issue with quotation here that required disabling it?