Changed environment definition, added an inductive env_consistent, and
added some theorems and proofs in the Sanity section