Вызвать статическое подключение библиотеки, связанной с целью XCode?

Проблема не в том, что Coq не может угадать, какое значение использовать для m и n, а в том, что ваша цель не имеет правильной формы для создания этой теоремы. Когда вы пишете apply eq_add_S, Coq пытается объединить S n = S m -> n = m с S (add i j) = S (add i k) -> j = k, что не может быть сделано.

Вам нужно применить eq_add_S к предпосылке предпосылки , введя ее в контекст.

Proof.
intros i j k H. (* H : add i j = add i k *)
induction i as [|i IH].
- apply H.
- apply eq_add_S in H.
  (* ...  *)