∀ (motive : Lean.Level → Lean.Level → Sort u_1) (α : Sort u✝) (β : α → Sort v✝) (f : (x : α) → β x)
  (rel : Lean.Level → Lean.Level → α → Prop) (u v : Lean.Level)
  (h_1 : Unit → ((y : α) → rel Lean.Level.zero Lean.Level.zero y → β y) → motive Lean.Level.zero Lean.Level.zero)
  (h_2 : (u v : Lean.Level) → ((y : α) → rel u.succ v.succ y → β y) → motive u.succ v.succ)
  (h_3 : (a : Lean.Level) → ((y : α) → rel Lean.Level.zero a.succ y → β y) → motive Lean.Level.zero a.succ)
  (h_4 : (a : Lean.Level) → ((y : α) → rel a.succ Lean.Level.zero y → β y) → motive a.succ Lean.Level.zero)
  (h_5 :
    (v₁ v₂ : Lean.Level) → ((y : α) → rel Lean.Level.zero (v₁.max v₂) y → β y) → motive Lean.Level.zero (v₁.max v₂))
  (h_6 :
    (u₁ u₂ : Lean.Level) → ((y : α) → rel (u₁.max u₂) Lean.Level.zero y → β y) → motive (u₁.max u₂) Lean.Level.zero)
  (h_7 : (a v : Lean.Level) → ((y : α) → rel Lean.Level.zero (a.imax v) y → β y) → motive Lean.Level.zero (a.imax v))
  (h_8 : (a u : Lean.Level) → ((y : α) → rel (a.imax u) Lean.Level.zero y → β y) → motive (a.imax u) Lean.Level.zero)
  (h_9 : (u₁ u₂ v₁ v₂ : Lean.Level) → ((y : α) → rel (u₁.max u₂) (v₁.max v₂) y → β y) → motive (u₁.max u₂) (v₁.max v₂))
  (h_10 :
    (u₁ u₂ v₁ v₂ : Lean.Level) → ((y : α) → rel (u₁.imax u₂) (v₁.imax v₂) y → β y) → motive (u₁.imax u₂) (v₁.imax v₂))
  (h_11 :
    (uName : Lean.Name) →
      (x : Lean.Level) → ((y : α) → rel (Lean.Level.param uName) x y → β y) → motive (Lean.Level.param uName) x)
  (h_12 :
    (a : Lean.LMVarId) →
      (x : Lean.Level) → ((y : α) → rel (Lean.Level.mvar a) x y → β y) → motive (Lean.Level.mvar a) x)
  (h_13 :
    (x : Lean.Level) →
      (a : Lean.LMVarId) → ((y : α) → rel x (Lean.Level.mvar a) y → β y) → motive x (Lean.Level.mvar a))
  (h_14 : (x x_1 : Lean.Level) → ((y : α) → rel x x_1 y → β y) → motive x x_1),
  ((match (motive := (u v : Lean.Level) → ((y : α) → rel u v y → β y) → motive u v) u, v with
      | Lean.Level.zero, Lean.Level.zero => fun x => h_1 a x
      | u.succ, v.succ => fun x => h_2 u v x
      | Lean.Level.zero, a.succ => fun x => h_3 a x
      | a.succ, Lean.Level.zero => fun x => h_4 a x
      | Lean.Level.zero, v₁.max v₂ => fun x => h_5 v₁ v₂ x
      | u₁.max u₂, Lean.Level.zero => fun x => h_6 u₁ u₂ x
      | Lean.Level.zero, a.imax v => fun x => h_7 a v x
      | a.imax u, Lean.Level.zero => fun x => h_8 a u x
      | u₁.max u₂, v₁.max v₂ => fun x => h_9 u₁ u₂ v₁ v₂ x
      | u₁.imax u₂, v₁.imax v₂ => fun x => h_10 u₁ u₂ v₁ v₂ x
      | Lean.Level.param uName, x => fun x_1 => h_11 uName x x_1
      | Lean.Level.mvar a, x => fun x_1 => h_12 a x x_1
      | x, Lean.Level.mvar a => fun x_1 => h_13 x a x_1
      | x, x_1 => fun x_2 => h_14 x x_1 x_2)
      fun y h => f y) =
    match u, v with
    | Lean.Level.zero, Lean.Level.zero => h_1 a fun y h => f y
    | u.succ, v.succ => h_2 u v fun y h => f y
    | Lean.Level.zero, a.succ => h_3 a fun y h => f y
    | a.succ, Lean.Level.zero => h_4 a fun y h => f y
    | Lean.Level.zero, v₁.max v₂ => h_5 v₁ v₂ fun y h => f y
    | u₁.max u₂, Lean.Level.zero => h_6 u₁ u₂ fun y h => f y
    | Lean.Level.zero, a.imax v => h_7 a v fun y h => f y
    | a.imax u, Lean.Level.zero => h_8 a u fun y h => f y
    | u₁.max u₂, v₁.max v₂ => h_9 u₁ u₂ v₁ v₂ fun y h => f y
    | u₁.imax u₂, v₁.imax v₂ => h_10 u₁ u₂ v₁ v₂ fun y h => f y
    | Lean.Level.param uName, x => h_11 uName x fun y h => f y
    | Lean.Level.mvar a, x => h_12 a x fun y h => f y
    | x, Lean.Level.mvar a => h_13 x a fun y h => f y
    | x, x_1 => h_14 x x_1 fun y h => f y