[isabelle] prove countability of a new finite type



Hello,


i define 


datatype Colors = Red | Yellow | Green


How can i prove:


instance Colors :: countable 


?


Mathematically, id say the type is finite, so i would give an injection to the natural numbers. can you help me in isabelle?


Many thanks!
 		 	   		  


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