theorem proving - Relationship between existential and universal quantifier in an inductive Coq definition -

suppose want inductive definiton of substring (with string being synonym list).

inductive substring {a : set} (w : string a) :                     (string a) -> prop :=   | ss_substr : forall x y z : string a,                   x ++ y ++ z = w ->                   substring w y. 

here can example prove following:

theorem test : substring [3;4;1] [4]. proof.   eapply ss_substr.   cbn.   instantiate (1:=[1]).   instantiate (1:=[3]).   reflexivity. qed. 

however, proof "existential" rather "universal", in spite of fact inductive definition states forall x y z , constrains shapes. seems unintuitive me. gives?

also, possible make inductive definition using exists x : string a, exists y : string a, exists z : string, x ++ y ++ z = w -> substring w y?

one important thing note exists not built-in functionality of coq (contrary forall). actually, exists notation, behind there inductive type named ex. notation , inductive type defined in coq standard library. here definition of ex:

inductive ex (a:type) (p:a -> prop) : prop :=     ex_intro : forall x:a, p x -> ex (a:=a) p. 

it defined using 1 constructor , universal quantification, substring type, not surprising susbtring type seems "existential" @ point.

of course, can define type using exists, , not need inductive.

definition substring' {a : set} (w y : string a) : prop :=     exists x z, x ++ y ++ z = w.