X<Y, Y<Z -> X<Z.
X<X -> [].
X<Y, Y<X, X=Y.
X<Y -> X=<Y.
X=<Y -> X<Y,X=Y.
X=<X.

s(X)=s(Y) -> X=Y.
p(X)=p(Y) -> X=Y.
p(s(X))=X.
s(p(X))=X.


X<s(X).

X=<Y -> X<s(Y).