Renamed ~> to step and => to eval.
Added signatures to operational semantics.
Finished formalization with annotated terms.
Commented handler preservation lemma cases.