SymmetryBook
SymmetryBook copied to clipboard
more coercions needed?
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.