 Unravelling of a Kripke model

The unravelling of a rooted Kripke model has finite increasing paths from the root as worlds, ordered by extension and labelled by their endpoints. It is tree-like and preserves forcing.