for dl being Int_position holds dl <> IC