*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Proving a simple lemma*From*: Steve Wong <s.wong.731 at gmail.com>*Date*: Thu, 26 Jul 2012 20:10:12 +0100

Hi I'm struggling to prove the following lemma: lemma "EX k:S. P k == EX k. k : S --> P k" If my understand is right, the lemma should be correct. However, I can't find a proof using sledgehammer. Any help will be appreciated. Thanks. Steve

**Follow-Ups**:**Re: [isabelle] Proving a simple lemma***From:*Elsa L Gunter

**Re: [isabelle] Proving a simple lemma***From:*Tjark Weber

- Previous by Date: Re: [isabelle] skip_proofs in Isabelle2012
- Next by Date: Re: [isabelle] Proving a simple lemma
- Previous by Thread: [isabelle] Some more project announcements
- Next by Thread: Re: [isabelle] Proving a simple lemma
- Cl-isabelle-users July 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list