results of polymorphic functions may have a sort that looks like
Type _, even when the sort should actually be convertible with Prop _
This correction makes sort_cmp acknowledge this evolution