Level.inject done, proof automatized for push and inject in Level
Level: added pop and eject, and the related lemmas