* the local_context (which is the Rel moved to the canonical context).
* Typically, the list of optional terms is the explicit
* substitution that is applied to a metavariable occurrence and the result of
* the local_context (which is the Rel moved to the canonical context).
* Typically, the list of optional terms is the explicit
* substitution that is applied to a metavariable occurrence and the result of