Lambda seems to require [type_cast] to induce an equivalence relation.
Merge remote-tracking branch 'origin' into lambda
first push on adding polymorphism.

- The Ocaml module enables Ocaml-style polymorphism,
  i.e. Pi types range only over [*].
working on Poly.

- All of the admitted definitions are about dependent
  contexts.
- There should be a similar interface that abstracts
  the relevant bits for this but it isn't the same simple
  structures because they use [Pi] instead of [->]
two versions of dependent contexts...
progress on the lemmas for implementing procedures.
problem with contexts!

- types in the type context can depend on values in the kind
  context!
  - Fixes this requires a new notion of contexts (and breaks the
    functor completely).
  - Ultimately this should not be a functor. It can be partially
    evaluated later on.
- Bug fix in [typ_lift]
fixing contexts & implementation of Abs.
universe inconsistency

when instantiating a polymorphic type.
the kind of Pi is *
the rest of the kindof_typ pi fix.
fixing the universe problems (fingers crossed)

- there is no denotation function denoting expressions
  into typ0 because it seems to require unlifting which
  Coq does not permit.
finishing up Lambda2/ExprDIeq

- need to get stuff into shape but this is the main bit.
the rest of the proofs.

Next steps:
- Build an interface with the appropriate lemmas
- Build some tactics, e.g. exprD_rw
- Start the monad rewriter.
the start of the facts for Lambda2.
These functors do not work!

- I can not make an environment extension because the
  denotation function must be fully known before the functor
  is instantiated.
Moving some things around

- Renamed Lambda2 -> LambdaM
- Lambda will become the Lambda that doesn't use modules
  (modules seem to limit extension/composition a lot)
- Adding Readme.md to Poly/ Lambda/ LambdaM
- Examples do not currently compile!
Working on Lambda & Monad2

- ExprD and ExprDI and ExprCore in Lambda
- A few interface changes to Lambda/TypesI2
- Added MirrorCore.SymEnv which has a simple reference
  injection using a positive map.
- Implemented MonadSym with cases for return and bind.
- A few small test cases (without sanity checks)
- Fixes to MonadTypes.
monad reduction.
Moving lift and lower to Lamba/ExprLift.