| (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
reduce (k+1, m'::e, ens, t, s)
| (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
reduce (k+1, m'::e, ens, t, s)