use(lists).

goal ~ all(X,all(Y,all(Z,

   cons(X,Z)=cons(Y,Z) => X=Y

  ))).