cases c_in
L R : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
c_in : (insert (~φ') (L.erase (~(φ'⋀ψ'))), R) = c ∨ (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R) = c
α_in_L : ~(φ⋀ψ) ∈ L
⊢ ~(φ⋀ψ) ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1
case inl
L R : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
α_in_L : ~(φ⋀ψ) ∈ L
h✝ : (insert (~φ') (L.erase (~(φ'⋀ψ'))), R) = c
⊢ ~(φ⋀ψ) ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1

case inr
L R : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
α_in_L : ~(φ⋀ψ) ∈ L
h✝ : (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R) = c
⊢ ~(φ⋀ψ) ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1