- | C.LetIn (nname, vv, tyty, tt) when H.is_proof c v ->
- (*CSC: here we need the type of v *)
- let x = C.LetIn (nname, vv, tyty,
- C.LetIn (name, tt, assert false, 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 = H.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