for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s1, s2 being State of A st IC s1 = IC s2 & DataPart s1 = DataPart s2 holds
s1 = s2