% union is commutative



sub(X,Y)<=>all(Z,in(Z,X)=>in(Z,Y)).
eq(X,Y)<=>(sub(X,Y) and sub(Y,X)).
in(X,u(A,B)) <=> (in(X,A) or in(X,B)).


goal ~ all(A,all(B,eq(u(A,B),u(B,A)))).


precedence([eq,sub,in]).