Clarify that change algebra operations trivially preserve d.o.e.
Clarify that change algebra operations trivially preserve d.o.e.

Old-commit-hash: c11fb0c1abae938f0c7ec3dacff96f112f6bbee4

inc-lc/ilc-agda