(motive :
    DoResultPR (List Lean.MVarId × Array Lean.Syntax) (List ⟨Lean.MVarId, pure⟩.fst × Array Lean.Syntax) PUnit.{1} →
      Sort u_1) →
  (r : DoResultPR (List Lean.MVarId × Array Lean.Syntax) (List ⟨Lean.MVarId, pure⟩.fst × Array Lean.Syntax) PUnit.{1}) →
    ((a : List Lean.MVarId × Array Lean.Syntax) → (u : PUnit.{1}) → motive (DoResultPR.pure a u)) →
      ((b : List ⟨Lean.MVarId, pure⟩.fst × Array Lean.Syntax) → (u : PUnit.{1}) → motive (DoResultPR.return b u)) →
        motive r