let _, context, _ = CicUtil.lookup_meta goal metasenv in
let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
let lemma = FNG.clean_dummy_dependent_types lemma in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
let lemma = FNG.clean_dummy_dependent_types lemma in