World subsumption is a sufficient condition that a metatheorem proved for one set of LF contexts can be reused in another set of contexts.
Eventually, this page will contain a self-contained explanation for world subsumption. For now, please read the discussion in Proving totality assertions in non-empty contexts in the tutorial Proving metatheorems with Twelf and on the %worlds page.
This page is incomplete. We should expand it.