Rewrote the application rules to 

e' --> e''
-------------
e e' --> e e''

e --> e'
-------------
e v --> e' v

To match the semantics of bind. To show the monadic law
ret a >>= f   =   f a
It has to evaluate a first.