let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let change subst where terms metasenv ugraph =
if terms = [] then where, metasenv, ugraph
let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let change subst where terms metasenv ugraph =
if terms = [] then where, metasenv, ugraph