intro P
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
⊢ ∀ (P : Formula), (P ∈ ↑X → evaluate (↑MG) X P) ∧ ((~P) ∈ ↑X → ¬evaluate (↑MG) X P)
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P : Formula
⊢ (P ∈ ↑X → evaluate (↑MG) X P) ∧ ((~P) ∈ ↑X → ¬evaluate (↑MG) X P)