let metasenv, metano, instance, _ =
NCicMetaSubst.mk_meta ?name metasenv ctx (`WithType ty) in
let metasenv = List.filter (fun j,_ -> j <> metano) metasenv in
let subst = (metano, (name, ctx, bo_, ty)) :: subst in
let metasenv, metano, instance, _ =
NCicMetaSubst.mk_meta ?name metasenv ctx (`WithType ty) in
let metasenv = List.filter (fun j,_ -> j <> metano) metasenv in
let subst = (metano, (name, ctx, bo_, ty)) :: subst in