∀ (motive : Lean.Expr → Sort u_1) (α : Sort u✝) (β : α → Sort v✝) (f : (x : α) → β x) (rel : Lean.Expr → α → Prop)
  (e : Lean.Expr)
  (h_1 :
    (name : Lean.Name) →
      (us : List Lean.Level) → ((y : α) → rel (Lean.Expr.const name us) y → β y) → motive (Lean.Expr.const name us))
  (h_2 : (f x : Lean.Expr) → ((y : α) → rel (f.app x) y → β y) → motive (f.app x))
  (h_3 :
    (binderName : Lean.Name) →
      (ty body : Lean.Expr) →
        (binderInfo : Lean.BinderInfo) →
          ((y : α) → rel (Lean.Expr.forallE binderName ty body binderInfo) y → β y) →
            motive (Lean.Expr.forallE binderName ty body binderInfo))
  (h_4 : Unit → ((y : α) → rel (Lean.Expr.sort Lean.Level.zero) y → β y) → motive (Lean.Expr.sort Lean.Level.zero))
  (h_5 : (a : Lean.Level) → ((y : α) → rel (Lean.Expr.sort a.succ) y → β y) → motive (Lean.Expr.sort a.succ))
  (h_6 : (u : Lean.Level) → ((y : α) → rel (Lean.Expr.sort u) y → β y) → motive (Lean.Expr.sort u))
  (h_7 : (x : Lean.Expr) → ((y : α) → rel x y → β y) → motive x),
  ((match (motive := (e : Lean.Expr) → ((y : α) → rel e y → β y) → motive e) e with
      | Lean.Expr.const name us => fun x => h_1 name us x
      | f.app x => fun x_1 => h_2 f x x_1
      | Lean.Expr.forallE binderName ty body binderInfo => fun x => h_3 binderName ty body binderInfo x
      | Lean.Expr.sort Lean.Level.zero => fun x => h_4 a x
      | Lean.Expr.sort a.succ => fun x => h_5 a x
      | Lean.Expr.sort u => fun x => h_6 u x
      | x => fun x_1 => h_7 x x_1)
      fun y h => f y) =
    match e with
    | Lean.Expr.const name us => h_1 name us fun y h => f y
    | f_1.app x => h_2 f_1 x fun y h => f y
    | Lean.Expr.forallE binderName ty body binderInfo => h_3 binderName ty body binderInfo fun y h => f y
    | Lean.Expr.sort Lean.Level.zero => h_4 a fun y h => f y
    | Lean.Expr.sort a.succ => h_5 a fun y h => f y
    | Lean.Expr.sort u => h_6 u fun y h => f y
    | x => h_7 x fun y h => f y