在Coq中使用Vectors应用引理遇到的类型合一问题

已证明的基础引理 #

Lemma exists_distribution: 
forall (a:Prop)(Omega:Set)(p:Omega->Prop),
(exists x:Omega, p x->a)<->
((exists x:Omega,~(p x))\/(exists x:Omega,a)).

通用版本引理 #

为使p能接受任意数量的Omega参数，我证明了该引理的通用版本：

Require Import Coq.Vectors.Vector.
Import VectorNotations.


Lemma exists_distribution_n: 
forall (a:Prop)(n:nat)(Omega:Set)(p:Vector.t Omega n->Prop),
(exists x:Vector.t Omega n, p x->a)<->
((exists x:Vector.t Omega n,~(p x))\/(exists x:Vector.t Omega n,a)).

引理应用失败问题 #

尝试将上述通用引理应用到以下引理时，Coq提示无法合一表达式：

Lemma implication: 
forall (a: Prop) (Omega:Set) (p: Omega->Prop), 
exists x :Omega, 
p x  -> a.

请问我的方法是否有误？

Vector类型等价性疑问 #

另外，当n=3时，p:Vector.t Omega n->Prop等价于p:Omega->Omega->Omega->Prop还是p:Omega* Omega* Omega->Prop？

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