| v when H.is_proof c v && H.is_atomic v ->
let x = S.subst v t in
opt_proof g (info st "Optimizer: remove 5") true c x
- | v ->
+(* | v when t = C.Rel 1 ->
+ g (info st "Optimizer: remove 6") v
+*) | v ->
g st (C.LetIn (name, v, w, t))
in
if es then opt_term g st es c v else g st v