let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let selected_hyps,terms_with_context =
ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
- assert (selected_hyps = []);
let typ,term =
match terms_with_context, term with
[], None ->