(motive : Lean.Meta.Grind.SplitInfo → Lean.Meta.Grind.SplitInfo → Sort u_1) →
  (x x_1 : Lean.Meta.Grind.SplitInfo) →
    ((e₁ : Lean.Expr) →
        (source : Lean.Meta.Grind.SplitSource) →
          (e₂ : Lean.Expr) →
            (source_1 : Lean.Meta.Grind.SplitSource) →
              motive (Lean.Meta.Grind.SplitInfo.default e₁ source) (Lean.Meta.Grind.SplitInfo.default e₂ source_1)) →
      ((e₁ : Lean.Expr) →
          (h : e₁.isForall = true) →
            (source : Lean.Meta.Grind.SplitSource) →
              (e₂ : Lean.Expr) →
                (h_2 : e₂.isForall = true) →
                  (source_1 : Lean.Meta.Grind.SplitSource) →
                    motive (Lean.Meta.Grind.SplitInfo.imp e₁ h source)
                      (Lean.Meta.Grind.SplitInfo.imp e₂ h_2 source_1)) →
        ((a b : Lean.Expr) →
            (i : ℕ) →
              (e₁ : Lean.Expr) →
                (source : Lean.Meta.Grind.SplitSource) →
                  (a_1 b_1 : Lean.Expr) →
                    (i_1 : ℕ) →
                      (e₂ : Lean.Expr) →
                        (source_1 : Lean.Meta.Grind.SplitSource) →
                          motive (Lean.Meta.Grind.SplitInfo.arg a b i e₁ source)
                            (Lean.Meta.Grind.SplitInfo.arg a_1 b_1 i_1 e₂ source_1)) →
          ((e : Lean.Expr) →
              (source : Lean.Meta.Grind.SplitSource) →
                (x : Lean.Meta.Grind.SplitInfo) → motive (Lean.Meta.Grind.SplitInfo.default e source) x) →
            ((e : Lean.Expr) →
                (h : e.isForall = true) →
                  (source : Lean.Meta.Grind.SplitSource) →
                    (x : Lean.Meta.Grind.SplitInfo) → motive (Lean.Meta.Grind.SplitInfo.imp e h source) x) →
              ((x x_2 : Lean.Meta.Grind.SplitInfo) → motive x x_2) → motive x x_1