let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in
let context_for_newmeta = None :: context in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context_for_newmeta in
let newmetaty = CicSubstitution.lift 1 ty in
let bo' = C.LetIn (fresh_name, term, C.Meta (newmeta,irl)) in
let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in
let context_for_newmeta = None :: context in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context_for_newmeta in
let newmetaty = CicSubstitution.lift 1 ty in
let bo' = C.LetIn (fresh_name, term, C.Meta (newmeta,irl)) in