(motive :
    DoResultPR (Option Lean.Meta.Grind.EMatchTheorem) (Option Lean.Meta.Grind.EMatchTheorem) PUnit.{1} → Sort u_1) →
  (r : DoResultPR (Option Lean.Meta.Grind.EMatchTheorem) (Option Lean.Meta.Grind.EMatchTheorem) PUnit.{1}) →
    ((a : Option Lean.Meta.Grind.EMatchTheorem) → (u : PUnit.{1}) → motive (DoResultPR.pure a u)) →
      ((b : Option Lean.Meta.Grind.EMatchTheorem) → (u : PUnit.{1}) → motive (DoResultPR.return b u)) → motive r