formalism: Relate the untyped and typed Hazelnut models

[mirryi]

We should have a metatheorem that relates the untyped and typed Hazelnut models.

To achieve this, we probably need a mark erasure operation on marked zippered expressions (which preserves the cursor). This should also allow some commutativity statement: applying cursor erasure then regular mark erasure gives the same unmarked expression as applying this new mark erasure then cursor erasure.

[mirryi]

This was resolved by #8.