[isabelle] Proofability of a simple existential statement

I have a quick, basic question: How come the following is provable, without
the need of any fact:

lemma exzero: "EX func arg. func arg = 0"
by auto

How are func and arg instantiated?

Thank you for any help in advance.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.