more coercions needed?

[DanGrayson]

Look at this:

I think we need more coercions if we want the type \bn n to be regarded as an element of all three of those types.