[isabelle] Silly problem with maps and

How do I prove the following? M is a map, l is just a type, which is why I explicitly included the premise that there was an l not in the domain. !! l . [| \<exists> l . l \<notin> dom M; l \<in> dom M |] ==> l \<noteq> (SOME l. l \<in> dom M)

I expect that I'm going to feel silly when somebody solves this for me (or explains why it's false), but, oh well. :-)

- John

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