λz,loc,L. if (∃l∈L.IdDeq l loc)_b then {L} else {[loc / L]} fi ∈ ∩A:Type. (A ─→ Id ─→ (Id List) ─→ bag(Id List))