The Coq mailing list

[Rene Vestergaard <vester AT jaist.ac.jp>]

Please find below an example development of deskolemisation. When 
invoking it, the specific P needs to be listed in addition to the 
formula being deskolemised. Is there a nice/standard alternative whose 
uses are implicit about the P?

Cheers,
/R

Section Deskolemise.

Variable A : Type.
Variable B : Type.
Variable P : A -> B -> Prop.

Theorem deskolemise : (exists F : A -> B, forall a : A , P a (F a))
                      -> forall a : A , exists b : B , P a b.
intro skolemised. elim skolemised.
intros F gConcl arg. exists (F arg). apply gConcl.
Qed.

End Deskolemise.