let (_,metasenv,_,_) = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
match (R.whd context ty) with
let (_,metasenv,_,_) = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
match (R.whd context ty) with