let _, context, _ = CicUtil.lookup_meta goal metasenv in
let tactic = elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback in
let old_context_length = List.length context in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let tactic = elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback in
let old_context_length = List.length context in