- | C.LetIn (nname, vv, tt) when H.is_proof c v ->
- let x = C.LetIn (nname, vv, C.LetIn (name, tt, S.lift_from 2 1 t)) in
+ | C.LetIn (nname, vv, ww, tt) when H.is_proof c v ->
+ let eentry = Some (nname, C.Def (vv, ww)) in
+ let ttw = get_type "opt1_letin 1" (eentry :: c) tt in
+ let x = C.LetIn (nname, vv, ww,
+ C.LetIn (name, tt, ttw, S.lift_from 2 1 t)) in