Put the reduction rules in the explainer

[dhil]

The explainer covers the static semantics of the proposed extension, but not so such its dynamic semantics. We do have the reduction rules scattered between an old document and in a comment on another issue. We should bring these together into the execution section of the explainer.

[fgmccabe]

Sounds good to me.