Porting ConCert to Metacoq v1.0+8.14

[annenkov]

The main difficulty was the tCase representation and the corresponding meta-theory.
All code and examples work. However, there are Admitted lemmas:

• in TypeAnnotations: a proof obligation related to tCase typing is admitted.
• Top-level statement in ExtractionCorrectness.v requires proofs that our recursive environment erasure produces a well-formed wf_glob environment.
  MetaCoq has a similar erasure function, but we can ignore dependencies which were remapped.
  Moreover, we not only erase terms but we apply our erasure for types and produce extended environment, containing typing information.
  So, we cannot just use MetaCoq environment erasure and its properties.
  I guess we need a bunch of lemmas that our way working with dependencies is the same as in MetaCoq.
  The best way is probably leave it for now and let MetaCoq team help us to integrate it.

Other issues:

• We use Coq's string from the stdlib, but MetaCoq uses bytestring that is copied from the BedRock project https://github.com/MetaCoq/metacoq/blob/coq-8.16/template-coq/theories/utils/bytestring.v.
  We should as MetaCoq developers, whether it's possible to put bytestring to opam, so we can use it for all our stuff as a dependency.
  For now, we convert between this representation back and forth, which is inefficient and annoying due to name/scope/... issues.

[annenkov]

I've created a branch coq-8.11 with the current state of master.

[annenkov]

@4ever2 should I do anything else before merging the PR?

[4ever2]

@4ever2 should I do anything else before merging the PR?

No, it should be ready to merge.