coq - 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

我想S从目标中删除 s ，获得目标n = m。有没有这样做的策略？

Answer 1

您正在寻找f_equal策略。