simp [Q, relate, Relation.Comp] at *
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
⊢ Q (↑MG).Rel (?'φ) X Y → relate (↑MG) (?'φ) X Y
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
φ : Formula
this : (φ ∈ ↑X → evaluate (↑MG) X φ) ∧ ((~φ) ∈ ↑X → ¬evaluate (↑MG) X φ)
⊢ X = Y → φ ∈ ↑X → X = Y ∧ evaluate (↑MG) X φ