∀ {R : Type u_1} [inst : Ring R] (motive : Polynomial R → (x : Polynomial R) → x.Monic → Sort u_2) (α : Sort u✝)
  (β : α → Sort v✝) (f : (x : α) → β x) (rel : Polynomial R → (x : Polynomial R) → x.Monic → α → Prop)
  (x x_1 : Polynomial R) (x_2 : x_1.Monic)
  (h_1 : (p q : Polynomial R) → (hq : q.Monic) → ((y : α) → rel p q hq y → β y) → motive p q hq),
  ((match (motive := (x x_3 : Polynomial R) → (x_4 : x_3.Monic) → ((y : α) → rel x x_3 x_4 y → β y) → motive x x_3 x_4)
        x, x_1, x_2 with
      | p, q, hq => fun x => h_1 p q hq x)
      fun y h => f y) =
    match x, x_1, x_2 with
    | p, q, hq => h_1 p q hq fun y h => f y