(motive : Lean.Expr → Sort u_1) →
  (x : Lean.Expr) →
    ((data : Lean.MData) → (e : Lean.Expr) → motive (Lean.Expr.mdata data e)) →
      ((typeName : Lean.Name) → (idx : ℕ) → (e : Lean.Expr) → motive (Lean.Expr.proj typeName idx e)) →
        ((e f a : Lean.Expr) → (h : e = f.app a) → motive (namedPattern e (f.app a) h)) →
          ((e : Lean.Expr) →
              (binderName : Lean.Name) →
                (d b : Lean.Expr) →
                  (binderInfo : Lean.BinderInfo) →
                    (h : e = Lean.Expr.lam binderName d b binderInfo) →
                      motive (namedPattern e (Lean.Expr.lam binderName d b binderInfo) h)) →
            ((e : Lean.Expr) →
                (binderName : Lean.Name) →
                  (d b : Lean.Expr) →
                    (binderInfo : Lean.BinderInfo) →
                      (h : e = Lean.Expr.forallE binderName d b binderInfo) →
                        motive (namedPattern e (Lean.Expr.forallE binderName d b binderInfo) h)) →
              ((e : Lean.Expr) →
                  (declName : Lean.Name) →
                    (t v b : Lean.Expr) →
                      (nondep : Bool) →
                        (h : e = Lean.Expr.letE declName t v b nondep) →
                          motive (namedPattern e (Lean.Expr.letE declName t v b nondep) h)) →
                ((declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us)) →
                  ((deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex)) →
                    ((u : Lean.Level) → motive (Lean.Expr.sort u)) →
                      ((a : Lean.Literal) → motive (Lean.Expr.lit a)) →
                        ((mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId)) →
                          ((fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId)) → motive x