let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let subst,metasenv,u,selected_hyps,terms_with_context =
ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let subst,metasenv,u,selected_hyps,terms_with_context =
ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph