% EAX
eq(X,X).                                % (reflexivity)
eq(X,Y) :- eq(Y,X).                     % (symmetry)    
eq(X,Y) :- eq(X,Z), eq(Z,Y).            % (transitivity)
eq(f(X1,X2,X3),f(Y1,Y2,Y3)) :-
     eq(X1,Y1), eq(X2,Y2), eq(X3,Y3).   % (substitutivity)