let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty,_ = (* TASSI: FIXME *)
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty,_ = (* TASSI: FIXME *)
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph