prove mlstring_lt is a StrongLinearOrder
Fix type_lt and prove type_cmp and term_cmp are total orders.

Mistake was using LIST_REL instead of LLEX.

By far the most difficult was showing that type_lt is transitive.
Required some hairy reasoning about LLEX cases. Not sure if there's a
better way.