List.fold_left
(fun (types, metasenv, subst, fl) (relevance,name,k,ty,bo) ->
let metasenv, subst, ty, _ = check_type metasenv subst [] ty in
List.fold_left
(fun (types, metasenv, subst, fl) (relevance,name,k,ty,bo) ->
let metasenv, subst, ty, _ = check_type metasenv subst [] ty in