universe elimination rules

Could someone tell me what are universe elimination rules in type theories.

Do they have something to do with quantifying or abstracting over universes?
Are there type systems which actually do this?

	Daniel Mahler

[All, Please send your replies to Daniel Mahler.
 Daniel Mahler, Please summarise your replies to the Types Forum.
  -- Philip Wadler, moderator, Types Forum.]