∀ {α : Type u_1} (motive : List (Poly α) → Sort u_2) (p : Poly α) (ps : List (Poly α)) (h_1 : Unit → motive [])
  (h_2 : (p : Poly α) → (ps : List (Poly α)) → motive (p :: ps)),
  (match p :: ps with
    | [] => h_1 ()
    | p :: ps => h_2 p ps) =
    h_2 p ps