Moving some lemmas into EnvI

- To share codee between Lambda and Ext
Adding reduction.

- beta_all should actually be reasonable complete, but probably
  really annoying to prove.
a few small notes.