{motive : Lean.Expr._impl → Sort u} →
  (t : Lean.Expr._impl) →
    ((data : Lean.Expr.Data) → (deBruijnIndex : ℕ) → motive (Lean.Expr.bvar._impl data deBruijnIndex)) →
      ((data : Lean.Expr.Data) → (fvarId : Lean.FVarId) → motive (Lean.Expr.fvar._impl data fvarId)) →
        ((data : Lean.Expr.Data) → (mvarId : Lean.MVarId) → motive (Lean.Expr.mvar._impl data mvarId)) →
          ((data : Lean.Expr.Data) → (u : Lean.Level) → motive (Lean.Expr.sort._impl data u)) →
            ((data : Lean.Expr.Data) →
                (declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const._impl data declName us)) →
              ((data : Lean.Expr.Data) → (fn arg : Lean.Expr) → motive (Lean.Expr.app._impl data fn arg)) →
                ((data : Lean.Expr.Data) →
                    (binderName : Lean.Name) →
                      (binderType body : Lean.Expr) →
                        (binderInfo : Lean.BinderInfo) →
                          motive (Lean.Expr.lam._impl data binderName binderType body binderInfo)) →
                  ((data : Lean.Expr.Data) →
                      (binderName : Lean.Name) →
                        (binderType body : Lean.Expr) →
                          (binderInfo : Lean.BinderInfo) →
                            motive (Lean.Expr.forallE._impl data binderName binderType body binderInfo)) →
                    ((data : Lean.Expr.Data) →
                        (declName : Lean.Name) →
                          (type value body : Lean.Expr) →
                            (nondep : Bool) → motive (Lean.Expr.letE._impl data declName type value body nondep)) →
                      ((data : Lean.Expr.Data) → (a : Lean.Literal) → motive (Lean.Expr.lit._impl data a)) →
                        ((data : Lean.Expr.Data) →
                            (data_1 : Lean.MData) →
                              (expr : Lean.Expr) → motive (Lean.Expr.mdata._impl data data_1 expr)) →
                          ((data : Lean.Expr.Data) →
                              (typeName : Lean.Name) →
                                (idx : ℕ) →
                                  (struct : Lean.Expr) → motive (Lean.Expr.proj._impl data typeName idx struct)) →
                            motive t