[isabelle] Proving a simple lemma


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.


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