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.