tauto
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
phi_in_X : φ ∈ ↑X
⊢ evaluate (↑MG) X φ
no goals