∀ (motive : Lean.Expr → Sort u_1) (α : Sort u✝) (β : α → Sort v✝) (f : (x : α) → β x) (rel : Lean.Expr → α → Prop)
  (e : Lean.Expr)
  (h_1 :
    (binderName : Lean.Name) →
      (t b : Lean.Expr) →
        (binderName_1 : Lean.Name) →
          (binderType body : Lean.Expr) →
            (binderInfo : Lean.BinderInfo) →
              (h : b = Lean.Expr.forallE binderName_1 binderType body binderInfo) →
                (binderInfo_1 : Lean.BinderInfo) →
                  ((y : α) →
                      rel
                          (Lean.Expr.forallE binderName t
                            (namedPattern b (Lean.Expr.forallE binderName_1 binderType body binderInfo) h) binderInfo_1)
                          y →
                        β y) →
                    motive
                      (Lean.Expr.forallE binderName t
                        (namedPattern b (Lean.Expr.forallE binderName_1 binderType body binderInfo) h) binderInfo_1))
  (h_2 : (e : Lean.Expr) → ((y : α) → rel e y → β y) → motive e),
  ((match (motive := (e : Lean.Expr) → ((y : α) → rel e y → β y) → motive e) e with
      | Lean.Expr.forallE binderName t (b@h:(Lean.Expr.forallE binderName_1 binderType body binderInfo)) binderInfo_1 =>
        fun x => h_1 binderName t b binderName_1 binderType body binderInfo h binderInfo_1 x
      | e => fun x => h_2 e x)
      fun y h => f y) =
    match e with
    | Lean.Expr.forallE binderName t (b@h:(Lean.Expr.forallE binderName_1 binderType body binderInfo)) binderInfo_1 =>
      h_1 binderName t b binderName_1 binderType body binderInfo h binderInfo_1 fun y h => f y
    | e => h_2 e fun y h => f y