let sort = match PEH.split_with_whd (context, ty_ty) with
| (_, C.Sort sort) ::_ , _ -> CicPp.ppsort sort
| (_, C.Meta _) :: _, _ -> CicPp.ppsort (C.Type (Un.fresh ()))
let sort = match PEH.split_with_whd (context, ty_ty) with
| (_, C.Sort sort) ::_ , _ -> CicPp.ppsort sort
| (_, C.Meta _) :: _, _ -> CicPp.ppsort (C.Type (Un.fresh ()))