(motive : Lean.Expr → Sort u_1) →
  (e : Lean.Expr) →
    ((u : Lean.Level) → motive (Lean.Expr.sort u)) →
      ((fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId)) →
        ((deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex)) →
          ((a : Lean.Literal) → motive (Lean.Expr.lit a)) →
            ((n : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const n us)) →
              ((mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId)) →
                ((data : Lean.MData) → (a : Lean.Expr) → motive (Lean.Expr.mdata data a)) →
                  ((fn arg : Lean.Expr) → motive (fn.app arg)) →
                    ((n : Lean.Name) → (t b : Lean.Expr) → (bi : Lean.BinderInfo) → motive (Lean.Expr.lam n t b bi)) →
                      ((n : Lean.Name) →
                          (t b : Lean.Expr) → (bi : Lean.BinderInfo) → motive (Lean.Expr.forallE n t b bi)) →
                        ((n : Lean.Name) →
                            (t v b : Lean.Expr) → (nondep : Bool) → motive (Lean.Expr.letE n t v b nondep)) →
                          ((typeName : Lean.Name) → (i : ℕ) → (s : Lean.Expr) → motive (Lean.Expr.proj typeName i s)) →
                            motive e