{α : Type} →
  (motive : Std.Internal.Parsec.ParseResult α (Sigma String.Pos) → Sort u_1) →
    (x : Std.Internal.Parsec.ParseResult α (Sigma String.Pos)) →
      ((pos : Sigma String.Pos) → (res : α) → motive (Std.Internal.Parsec.ParseResult.success pos res)) →
        ((it : Sigma String.Pos) →
            (err : Std.Internal.Parsec.Error) → motive (Std.Internal.Parsec.ParseResult.error it err)) →
          motive x