{motive : Lean.Expr → Sort u} →
  (t : Lean.Expr) →
    ((typeName : Lean.Name) → (idx : ℕ) → (struct : Lean.Expr) → motive (Lean.Expr.proj typeName idx struct)) →
      ((binderName : Lean.Name) →
          (binderType body : Lean.Expr) →
            (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName binderType body binderInfo)) →
        ((binderName : Lean.Name) →
            (binderType body : Lean.Expr) →
              (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.lam binderName binderType body binderInfo)) →
          ((declName : Lean.Name) →
              (type value body : Lean.Expr) →
                (nondep : Bool) → motive (Lean.Expr.letE declName type value body nondep)) →
            ((fn arg : Lean.Expr) → motive (fn.app arg)) →
              ((data : Lean.MData) → (expr : Lean.Expr) → motive (Lean.Expr.mdata data expr)) →
                ((declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us)) →
                  ((u : Lean.Level) → motive (Lean.Expr.sort u)) →
                    ((mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId)) →
                      (Nat.hasNotBit 3580 t.ctorIdx → motive t) → motive t