let levels_of_term metasenv context term =
let module TC = CicTypeChecker in
let module Red = CicReduction in
let levels_of_term metasenv context term =
let module TC = CicTypeChecker in
let module Red = CicReduction in
degree_aux (Red.whd context u)
in
let entry_eq (s1, b1, v1) (s2, b2, v2) =
degree_aux (Red.whd context u)
in
let entry_eq (s1, b1, v1) (s2, b2, v2) =