(motive : Lean.Expr → List Lean.Expr → Sort u_1) →
  (f : Lean.Expr) →
    (args : List Lean.Expr) →
      ((f : Lean.Expr) → motive f []) →
        ((binderName : Lean.Name) →
            (binderType b : Lean.Expr) →
              (binderInfo : Lean.BinderInfo) →
                (a : Lean.Expr) →
                  (as : List Lean.Expr) → motive (Lean.Expr.lam binderName binderType b binderInfo) (a :: as)) →
          ((n : Lean.Name) →
              (t v b : Lean.Expr) →
                (nondep : Bool) → (args : List Lean.Expr) → motive (Lean.Expr.letE n t v b nondep) args) →
            ((data : Lean.MData) → (b : Lean.Expr) → (args : List Lean.Expr) → motive (Lean.Expr.mdata data b) args) →
              ((f : Lean.Expr) → (args : List Lean.Expr) → motive f args) → motive f args