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策略。