let (curi,metasenv,proofbo,proofty) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let (curi,metasenv,proofbo,proofty) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in