Re: [isabelle] Proving a simple lemma
This is not true. "EX k : S . P K" is equivalent to "EX k. ((k : S) &
(P k))" , which is stronger than "EX k. k : S --> P k". If S is empty,
"EX k. k : S --> P k" is true, but "EX k : S . P K" is false.
On 7/26/12 2:10 PM, Steve Wong wrote:
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