new theorem about exprD' and equal (but different) variable
environments.
fixing compilation when things are not installed.
adding a new lemma about lift.
Merge branch 'master' of github.com:gmalecha/mirror-core
fixing the Makefile to avoid +=
fixing the examples + adding a builder for [types]
typo + comment about bugs.
compatibility with ocaml 3.12

- remove call to List.mapi
Expose the environments in Sem_equiv.
EProver interface

+ EProvers are like regular provers but can instantiate
  unification variables.
fix the naming of Prover/EProver

- Avoid the word "correct" because it means more than sound.
removing Separation Logic demo

- this is now in MirrorCharge
Adding a convenience lemma to avoid breaking the typeof_env abstraction.
generalizing to support an arbitrary equivalence relation on terms

- this is necessary to do unification modulo conversion.
Merge branch 'master' of github.com:gmalecha/mirror-core
a new AutoProver (currently without proof).

- A new lemma for nth_error and join_env.
Generalizing the Prover interface to support more types of predicates.

- Fixes Bug #10
- Will now support ILogics
- Expanding this even further could unify a lot more ideas,
  at the limit, this is just a "thing that reasons with known facts."
typo in EProver specification
Making unification an EProver

- Solves bug #8
tweaking EProverOk and ProverOk so that they take uvars first.