∀ {R : Type u_1} [inst : Ring R] (motive : Polynomial R → (x : Polynomial R) → x.Monic → Sort u_2) (p q : Polynomial R)
  (hq : q.Monic) (h_1 : (p q : Polynomial R) → (hq : q.Monic) → motive p q hq),
  (match p, q, hq with
    | p, q, hq => h_1 p q hq) =
    h_1 p q hq