Coq：从目标的两侧删除构造函数

Question

考虑以下部分证明：

Theorem test : forall (n m : nat),
  n = m -> S n = S m.
Proof.
  intros n m H.

执行到这一步会得到以下结果：

1 subgoal
n, m : nat
H : n = m
______________________________________(1/1)
S n = S m

我想从目标中删除 Ss，获得目标 n = m。有这样的策略吗？

Answer 1

您正在寻找 f_equal 策略。