Implemented instance of strict total order for types, based on strict total order for universes.
Removed implementation of irrefl-T.
Fixed error I introduced by removing A=B->|A|=|B|.
Mucked about in SC.Decidable.
[auto] merge master into gh-pages
[auto] updated html listings