let subst, metasenv, _ugraph, _conjecture, selected_terms =
ProofEngineHelpers.select
~metasenv ~ugraph ~conjecture:(0, context, pred) ~pattern
let subst, metasenv, _ugraph, _conjecture, selected_terms =
ProofEngineHelpers.select
~metasenv ~ugraph ~conjecture:(0, context, pred) ~pattern