Revisit the positive example

Stopped on this because the world ended and the POPL deadline didn't change---revisit this example since it might help folks understand changes to non-isomorphic types stuffed into equivalences a bit better.