我一直在各种场景中尝试apply策略，当前提如下时，它似乎卡在以下情况下：
H1 : a
H2 : a -> forall e : nat, b -> g e
============================
...
当我尝试apply H2 in H1.时，它给了我错误：
Error: Unable to find an instance for the variable e.
我以任何方式将forall e : nat, b -> g e作为场所的一部分。这是上述场景的完整工作代码：
Lemma test : forall {a b c : Prop} {g : nat} (f : nat -> Prop),
a / (a -> forall {e : nat}, b -> f e) -> c.
Proof.
intros a b c f g.
intros [H1 H2].
(* apply H2 in H1. *)
Abort.
Coq参考手册，§8.2.5：
术语
in识别apply策略试图将识别类型的结论与术语类型的非依赖前提相匹配，从右到左尝试它们。如果成功，则假设识别的陈述将替换为术语类型的结论。
现在，将上述描述应用于您的案例，我们得到以下内容，Coq 试图用H2的结论替换H1 : a，即g e.为此，它需要实例化具有某个值的通用量化变量e，Coq无法明显推断出该值 - 因此您看到了错误消息。
另一种查看方法是尝试apply ... in ...的不同变体：
eapply H2 in H1.
这将为您提供两个子目标：
...
H2 : a -> forall e : nat, b -> g e
H1 : g ?e
============================
c
和
...
H1 : a
H2 : a -> forall e : nat, b -> g e
============================
b
第一个子目标的H1假设显示了Coq使用普通apply in策略的目的，但在eapply in的情况下，变量e被存在变量(?e)所取代。如果你还不熟悉存在变量，那么它们是你向Coq做出的承诺，你以后会为它们构建术语。您应该通过统一隐式构建术语。
无论如何，specialize (H2 H1).可能是你想做的，或者类似的事情
pose proof (H2 H1) as H; clear H1; rename H into H1.