unify(X,Y) :-
      nonvar(Y), Y=s(T),
      unify(S,T),
      (  S=zero, X=one;
         S=one,  X=even;
         S=even, X=odd;
         S=odd,  X=even
      ).

  unify(zero,Y) :-
      Y==0.
  unify(X,Y) :-
      (Y==even; Y==odd; Y==zero; Y==one),
      X=Y.
  unify(X,Y) :-
      var(Y),
      X=Y.