相关疑难解决方法(0)

说我有以下关系：

Inductive my_relation: nat -> Prop :=
constr n: my_relation n.

我想证明以下几点：

Lemma example:
  (forall n, my_relation n -> my_relation (S n)) -> (exists n, my_relation n) -> exists n, my_relation (S n).
Proof.
  intros.

介绍之后，我具有以下环境：

1 subgoal
H : forall n : nat, my_relation n -> my_relation (S n)
H0 : exists n : nat, my_relation n
______________________________________(1/1)
exists n : nat, my_relation (S n)

我的问题是：是否有可能在存在量词下重写H？如果不是，是否有解决此类问题的策略（该特定问题并非真正相关，但是存在的问题是您必须证明exists使用另一种问题exists，并且在非正式情况下可以“推论”一种方法来重写该问题）exists。假设进入exists目标）？

例如，如果尝试尝试rewrite H in H0. …