let _,metasenv,_,_ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
let _,metasenv,_,_ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty = (CicTypeChecker.type_of_aux' metasenv context term) in