intro X P
Worlds : Set (Finset Formula)
MG : ModelGraph Worlds
⊢ ∀ (X : ↑Worlds), ∀ P ∈ ↑X, Evaluate (↑MG, X) P
Worlds : Set (Finset Formula)
MG : ModelGraph Worlds
X : ↑Worlds
P : Formula
⊢ P ∈ ↑X → Evaluate (↑MG, X) P