# Re: [isabelle] "PROOF FAILED for depth4"

On Thu, Apr 8, 2010 at 12:34 PM, Alexander Krauss <krauss at in.tum.de> wrote:
> > lemma te_zero: "EX func t. func t = 0"
>> >
>> > proof (intro exI)
>> >
>> > show "F s = 0"
>> >
>> >
>>
>> Thanks for the help. Unfortunately, I get an error from this, saying that
>> it can't solve goal by exported rule: F s = 0. Any hint on this will be
>> appreciated.
>>
>
> You may need to add type annotations to make sure that the types in your
> lemma statement are not more general than you want. Switch on "Isabelle ->
> Settings -> Show Types".
>
>
I see. However, why can't the types in the lemma be more general even the
function is existentially quantified? Can't a' and b' be instantiated to
real for F s = 0 in the proof?
Thanks
Steve
> Alex
>

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