let st, hyp, rqv = match get_inner_types st what, get_inner_types st v with
| Some (C.ALetIn _, _), _ ->
st, C.Def (H.cic v, H.cic w), [T.Intros (Some 1, [intro], dtext)]
let st, hyp, rqv = match get_inner_types st what, get_inner_types st v with
| Some (C.ALetIn _, _), _ ->
st, C.Def (H.cic v, H.cic w), [T.Intros (Some 1, [intro], dtext)]