[isabelle] prove countability of a new finite type


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.