refactor(library/algebra/order): change strong order pair, adopt new naming conventions
refactor(library/algebra): use new naming conventions, add information to speed up proofs
fix(library/unifier): assertion violation
fix(library/unifier): assertion violation