(motive :
    Array (Array Mathlib.Tactic.LibraryRewrite.RewriteInterface × Mathlib.Tactic.LibraryRewrite.Kind) ×
        Array (Array Mathlib.Tactic.LibraryRewrite.RewriteInterface × Mathlib.Tactic.LibraryRewrite.Kind) →
      Sort u_1) →
  (__discr :
      Array (Array Mathlib.Tactic.LibraryRewrite.RewriteInterface × Mathlib.Tactic.LibraryRewrite.Kind) ×
        Array (Array Mathlib.Tactic.LibraryRewrite.RewriteInterface × Mathlib.Tactic.LibraryRewrite.Kind)) →
    ((filtered all :
          Array (Array Mathlib.Tactic.LibraryRewrite.RewriteInterface × Mathlib.Tactic.LibraryRewrite.Kind)) →
        motive (filtered, all)) →
      motive __discr