(* Assumption: the term bo must be closed in the current context *)
let (_,metasenv,_,_) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
(* Assumption: the term bo must be closed in the current context *)
let (_,metasenv,_,_) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in