Termini invertibili da un lato nel lambda-beta-eta-calcolo con applicazioni nella programmazione funzionale.