apply h
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_in : (f ∈ L ∨ f ∈ R) ∨ (∃ a, O = some (Sum.inl a) ∧ (~unload a.1) = f) ∨ ∃ b, O = some (Sum.inr b) ∧ (~unload b.1) = f
⊢ f ∈ ↑w
case h.a
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_in : (f ∈ L ∨ f ∈ R) ∨ (∃ a, O = some (Sum.inl a) ∧ (~unload a.1) = f) ∨ ∃ b, O = some (Sum.inr b) ∧ (~unload b.1) = f
⊢ f ∈ L.toFinset ∪ (R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset)