(motive : Lean.Expr → Sort u_1) →
  (major : Lean.Expr) →
    ((majorFn : Lean.Name) →
        (us : List Lean.Level) →
          (arg arg_1 majorArg : Lean.Expr) → motive ((((Lean.Expr.const majorFn us).app arg).app arg_1).app majorArg)) →
      ((x : Lean.Expr) → motive x) → motive major