setD_closed and setDI_closed

[affeldt-aist]

measure.v defines the following:

Definition setD_closed := forall A B, B `<=` A -> G A -> G B -> G (A `\` B).
Definition setDI_closed := forall A B, G A -> G B -> G (A `\` B).

Isn't setDI_closed weird since the definition does not use setI?
Shouldn't it be setD_closed.
Then, what about renaming the now-old setD_closed to setSD_closed (with S for subset)?