Coq证明中如何用单行语句处理含exists的公理调用？

我在Coq里的理论最初有这么一条公理：

Axiom context_existence : forall s t a,
  F a s -> Ps t a -> exists u, C u s t.

当时用的时候直接一行就能搞定：

pose proof (context_existence s t a Fas Psta) as (u & Cust).

后来因为a没出现在公理结论里，我把公理重构了：

Axiom context_existence : forall s t,
  (exists a, F a s /\ Ps t a) -> exists u, C u s t.

又因为exists a, F a s /\ Ps t a这个式子在我的理论里有特定含义，我定义了一个谓词Cb：

Definition Cb s t := exists a, F a t /\ Ps s a.

最后公理改成了这样：

Axiom context_existence : forall s t,
  Cb t s -> exists u, C u s t.

但现在用起来就不直观了，得拆成两步：

pose proof (context_existence s t) as (u & Cust).
exists a; split; auto.

我知道合取可以用conj直接构造证据，比如这种写法：

pose proof (context_existence s t (conj Fas Psta)) as (u & Cust).

但现在涉及到存在量词，不知道有没有类似的构造函数能让我用单行语句完成证明？

有的，Coq里对应存在量词的构造函数是ex_intro，它的作用就是把具体的实例a，加上该实例满足谓词的证据，打包成exists a, ...形式的命题证据。结合conj一起用，就能写出单行的证明语句：

pose proof (context_existence s t (ex_intro _ _ a (conj Fas Psta))) as (u & Cust).

如果Coq能自动推断Cb t s对应的存在量词的类型参数，还可以简化成：

pose proof (context_existence s t (ex_intro _ a (conj Fas Psta))) as (u & Cust).

这样就不用拆分步骤，直接构造出Cb t s的证据传给公理，一步拿到u和对应的C u s t证据了。

内容的提问来源于stack exchange，提问作者Lepticed