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战术。