Module pred Import prop;

[Set=Prop];

$[Exists : {A|Set}(A->Prop)->Prop];
$[existsI : {A|Set}{P|A->Prop}{a:A}(P a)-> (Exists [x:A]P x)];
$[existsE : {A|Set}{P|A->Prop}{X|Prop}
		({a:A}(P a)->X)->(Exists [x:A]P x)->X];

[[A:Set][P:A->Prop][a:A][p:P a][X:Prop][f:{a:A}(P a)->X]
   existsE f (existsI a p) ==> f a p];