(motive : Std.Internal.Parsec.ParseResult (Array Mathlib.Tactic.Sat.LRATStep) (Sigma String.Pos) → Sort u_1) →
  (x : Std.Internal.Parsec.ParseResult (Array Mathlib.Tactic.Sat.LRATStep) (Sigma String.Pos)) →
    ((pos : Sigma String.Pos) →
        (steps : Array Mathlib.Tactic.Sat.LRATStep) → motive (Std.Internal.Parsec.ParseResult.success pos steps)) →
      ((x : Std.Internal.Parsec.ParseResult (Array Mathlib.Tactic.Sat.LRATStep) (Sigma String.Pos)) → motive x) →
        motive x