Prove equivalence for unpacking user-friendly types

[tlringer]

This still does not include lifting, more extensive testing, and so on. That will all come once in a later PR.