implement elimination of let bindings

including soundness proof