Successful validation chains

except_cases extracts a successful step from an Except computation. The error branch must contradict an existing success hypothesis; the tactic does not assume that validation succeeds.

def except_cases : Lean.ParserDescr

Split an intermediate Except result, using the enclosing computation's success to rule out the error branch. Unfold the enclosing computation in hOk first if necessary.

except_cases hf : f using hOk with value => ... provides hf : f = .ok value in the body. The error and payload types are unrestricted.