Theorem: modelExistence (Pdl/Completeness.lean)

State before:
X : TNode
⊢ consistent X → ∃ WS x W, X.toFinset ⊆ ↑W
Tactic:
sorry
State after:
no goals