`progress` fails on some goals

[sonmarcho]

The following fails:

example (x : U32) : ∃ (x' : U32), ok x' = x := by
  progress

In the following the goal for the else branch is left unproven:

example (x : U32) :
  ∃ x',
   (if x.val < U32.max then x + 1#u32
    else ok x) = ok x' := by
  progress*