exercise on type equivalence as a congruence, close #493
Merge pull request #558 from mikeshulman/tyeqcong

exercise on type equivalence as a congruence, close #493