have ⟨plus_R, minus_R⟩ := loadedTruthLemma MG X R
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
plus_Q : Q ∈ ↑X → evaluate (↑MG) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ (Q⋀R ∈ ↑X → evaluate (↑MG) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑MG) X (Q⋀R))
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
plus_Q : Q ∈ ↑X → evaluate (↑MG) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
plus_R : R ∈ ↑X → evaluate (↑MG) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑MG) X R
⊢ (Q⋀R ∈ ↑X → evaluate (↑MG) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑MG) X (Q⋀R))