move this implementation to eliminate_let.
- initial commit of eliminate_definition : the goal is
  to translate definitions by match into series of axioms.