I have proved the following

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)).

Now I would like to prove it for p taking an arbitrary number of arguments from Omega. So I assume the following would be the general case for the previous lemma

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)).

which I proved just fine. However I can’t apply it to the following

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

Coq says that it cannot unify the two expressions, is my approach the wrong one?

Assuming n=3 is p:Vector.t Omega n->Prop the same as p:Omega->Omega->Omega->Prop or p:Omega* Omega* Omega->Prop?