(motive : ℕ → Array Lean.Expr → ℕ → Array Lean.MVarId → Lean.Expr → Sort u_1) →
  (x : ℕ) →
    (x_1 : Array Lean.Expr) →
      (x_2 : ℕ) →
        (x_3 : Array Lean.MVarId) →
          (x_4 : Lean.Expr) →
            ((i : ℕ) →
                (args : Array Lean.Expr) →
                  (j : ℕ) →
                    (instMVars : Array Lean.MVarId) →
                      (n : Lean.Name) →
                        (d b : Lean.Expr) →
                          (bi : Lean.BinderInfo) → motive i args j instMVars (Lean.Expr.forallE n d b bi)) →
              ((i : ℕ) →
                  (args : Array Lean.Expr) →
                    (j : ℕ) → (instMVars : Array Lean.MVarId) → (type : Lean.Expr) → motive i args j instMVars type) →
                motive x x_1 x_2 x_3 x_4