def f : List Nat → List Nat :=
fun x =>
  match x with
  | a :: xs@h:(b :: bs) => xs
  | x => []