Update the generation of the backward functions so that they don't fail

[sonmarcho]

The backward functions now don't use the error monad anymore. For instance, the choose function used to be extracted to:

def choose
  {T : Type} (b : Bool) (x : T) (y : T) :
  Result (T × (T → Result (T × T)))
  :=
  if b
  then let back := fun ret => Result.ok (ret, y)
       Result.ok (x, back)
  else let back := fun ret => Result.ok (x, ret)
       Result.ok (y, back)

Now it gets compiled to:

def choose
  {T : Type} (b : Bool) (x : T) (y : T) :
  Result (T × (T → T × T))
  :=
  if b
  then let back := fun ret =>(ret, y)
       Result.ok (x, back)
  else let back := fun ret => (x, ret)
       Result.ok (y, back)