[isabelle] THE-operator



Hello,


i would like to prove the following:


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


It may well be a 1 line proof but unfortunately im unfamiliar with substitution on THE-operator).


Many thanks!
 		 	   		  


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