Most of these rules are preserving definedness because the update an existing association in a cell map.
The desugaring in the K compiler generates a map juxtaposition (partial, undefined for key collisions) in this case but the key is known to be already present.
Other rules are marked as preserving definedness because they use init*Cell functions without argument (assumed preserving, forthcoming change in the K compiler)
Most of these rules are preserving definedness because the update an existing association in a cell map. The desugaring in the K compiler generates a map juxtaposition (partial, undefined for key collisions) in this case but the key is known to be already present. Other rules are marked as preserving definedness because they use
init*Cellfunctions without argument (assumed preserving, forthcoming change in the K compiler)