Re: [isabelle] THE-operator



On 22.05.2013 16:13, Roger H. wrote:
i would like to prove the following:

   ( THE A. {a. f a = {c1, c2, c3}} = {a. f a = A}  )         =        {c1, c2, c3}

As you were already told on the -dev list, this theorem does not hold. Please read the answers you get.

  -- Lars




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