Re: [isabelle] SOME-operator



Hi Roger,

On 22.05.2013 20:51, Roger H. wrote:
> is this lemma true?
>
> lemma "Domain (SOME r. Domain r = {2,3}) = {2,3}"
>
> if yes, how can it be proved?

The approach I usually use is to prove "∃r. Domain r = {2, 3}" and then use the rule someI_ex.

 -- Lars




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