The Coq mailing list

["Jevgenijs Sallinens" <jevgenijs AT dva.lv>]

> Rene Vestergaard wrote:

> 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?

Dear Rene,

 

I hope the following could help by hiding P with coercion.

If nothing depends on specific structure of P, probably better to  declare it as global parameter.  

Regards,

Jevgenijs.

 

 

Section Deskolemise.

 

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

 

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

 

End Deskolemise.