Then our unit is naturally:
- let s_unit (a : 'a) : ('a state) = fun (s : store) -> (a, s)
+ let s_unit (a : 'a) : 'a state = fun (s : store) -> (a, s)
And we can reason our way to the bind function in a way similar to the reasoning given above. First, we need to apply `f` to the contents of the `u` box: