let ty = NCicTypeChecker.typeof status [] [] ctx t in
if is_a_fact status (mk_cic_term ctx ty) then
(debug_print(lazy("eq indexing " ^ (status#ppterm ctx [] [] ty)));
let ty = NCicTypeChecker.typeof status [] [] ctx t in
if is_a_fact status (mk_cic_term ctx ty) then
(debug_print(lazy("eq indexing " ^ (status#ppterm ctx [] [] ty)));