(motive : Lean.Expr → Sort u_1) →
  (type : Lean.Expr) →
    ((binderName : Lean.Name) → (d b : Lean.Expr) → (bi : Lean.BinderInfo) → motive (Lean.Expr.lam binderName d b bi)) →
      ((x : Lean.Expr) → motive x) → motive type