Agda: update description of Plotkin's context
Agda: update description of Plotkin's context

Reason: the previous description contains a modularization task
that is already partially carried out.

Reference:
https://github.com/ps-mr/ilc/commit/249e99d807e2382a37fb35aee78c235b98e427aa#commitcomment-3659727

Old-commit-hash: 3c52ba4a07600646db8de764b1460fa6b69c3014

inc-lc/ilc-agda