for dl being Int_position ex i being Nat st dl = DataLoc (i,0)