define mlstring_cmp from mlstring_lt
functional equations for type_cmp and term_cmp