Не удалось найти экземпляр для переменной

Контекст: я работаю над упражнениями в Software Foundations .

Theorem neg_move : forall x y : bool,
  x = negb y -> negb x = y.
Proof. Admitted.

Theorem evenb_n__oddb_Sn : forall n : nat,
  evenb n = negb (evenb (S n)).
Proof.
  intros n. induction n as [| n'].
  Case "n = 0".
    simpl. reflexivity.
  Case "n = S n'".
    rewrite -> neg_move.

Перед последней строкой моя подцель такова:

evenb (S n') = negb (evenb (S (S n')))

И я хочу преобразовать ее в следующее:

negb (evenb (S n')) = evenb (S (S n'))

Когда я пытаюсь пройти через rewrite -> neg_move , тем не менее, получается следующее ошибка:

Ошибка: невозможно найти экземпляр для переменной y.

Я уверен, что это действительно просто, но что я делаю не так? (Пожалуйста, не отдавайте ничего за решение evenb_n__oddb_Sn , если я не делаю это совершенно неправильно).