let con_sort = typeof status ~subst ~metasenv context te in
(match R.whd status ~subst context con_sort, R.whd status ~subst [] ty_sort with
(C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) ->
let con_sort = typeof status ~subst ~metasenv context te in
(match R.whd status ~subst context con_sort, R.whd status ~subst [] ty_sort with
(C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) ->