[isabelle] SOME-operator




Hello,


is this lemma true?


lemma "Domain (SOME r. Domain r = {2,3}) = {2,3}"


if yes, how can it be proved?


Thank you!


 		 	   		  


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