Lean: define the classical step through its partial recursive form

When a construction must later be shown computable in an oracle, define the classical step as pget (G a (decide Q1) (decide Q2)) a. Here G : St -> Bool -> Bool -> Part St is partial recursive, Q1, Q2 are the oracle questions, and pget p d := if h : p.Dom then p.get h else d (classical). Then the oracle proof is one application of a 'primitive recursion with a partial step, correct along the sequence' lemma. It needs only step a ∈ G a ..., which holds once an invariant gives Dom. Partrec has no cond/option_casesOn for partial branches. Avoid branching on partial computations: make the partial part uniform, e.g. evaluate gsp ... (bif isSplitLevel then ρ else []), where gsp [] = some [], then map a *computable* post-processing over it.