(motive : Lean.Expr → Sort u_1) →
  (x : Lean.Expr) →
    ((n : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const n us)) →
      ((n : Lean.Name) → (i : ℕ) → (struct : Lean.Expr) → motive (Lean.Expr.proj n i struct)) →
        ((fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId)) →
          ((mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId)) →
            ((binderName : Lean.Name) →
                (binderType body : Lean.Expr) →
                  (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName binderType body binderInfo)) →
              ((v : Lean.Literal) → motive (Lean.Expr.lit v)) →
                ((u : Lean.Level) → motive (Lean.Expr.sort u)) →
                  ((declName : Lean.Name) →
                      (type value body : Lean.Expr) →
                        (nondep : Bool) → motive (Lean.Expr.letE declName type value body nondep)) →
                    ((binderName : Lean.Name) →
                        (binderType body : Lean.Expr) →
                          (binderInfo : Lean.BinderInfo) →
                            motive (Lean.Expr.lam binderName binderType body binderInfo)) →
                      ((x : Lean.Expr) → motive x) → motive x