let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let (termty,metasenv',arguments,fresh_meta) =
ProofEngineHelpers.saturate_term
let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let (termty,metasenv',arguments,fresh_meta) =
ProofEngineHelpers.saturate_term