simp [modelCanSemImplyTNode, TNode.toFinset] at *
case h
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : TNode.toFinset (L, R, O) ⊆ ↑w
⊢ (↑M, w)⊨(L, R, O)
case h
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
WS : Finset (Finset Formula)
M : ModelGraph WS
w : { x // x ∈ WS }
h : L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset) ⊆ ↑w
⊢ ∀ (f : Formula),
    ((f ∈ L ∨ f ∈ R) ∨
        (∃ a, O = some (Sum.inl a) ∧ (~unload a.1) = f) ∨ ∃ b, O = some (Sum.inr b) ∧ (~unload b.1) = f) →
      evaluate (↑M) w f