Unravelling of a Kripke model
= 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.