Разрушение в результате применения функции предиката

Я новичок в Coq и у меня есть быстрый вопрос о тактике разрушения. Предположим, у меня есть функция count , которая подсчитывает количество вхождений данного натурального числа в список натуральных чисел:

Fixpoint count (v : nat) (xs : natlist) : nat :=
  match xs with
    | nil => 0
    | h :: t =>
      match beq_nat h v with
        | true => 1 + count v xs
        | false => count v xs
      end
  end.

Я бы хотел доказать следующую теорему:

Theorem count_cons : forall (n y : nat) (xs : natlist),
  count n (y :: xs) = count n xs + count n [y].

Если бы я доказывал Аналогичная теорема для n = 0, я мог бы просто разрушить y до 0 или S y '. В общем случае я бы хотел разрушить (beq_nat n y) до значения true или false, но я не могу заставить это работать - мне не хватает части синтаксиса Coq.

Есть идеи?