take i = (DataLoc (0,0)) := 1; :: thesis: i is shiftable
thus i is shiftable ; :: thesis: verum