formulas(goals).
all x all y all z ((IsIn(z,y) & x=y) -> IsIn(z,x)).
end_of_list.