simp at c_in
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
c_in : ∃ a ∈ [{~φ'}, {~ψ'}], (L \ {~(φ'⋀ψ')} ∪ a, R) = c
⊢ α ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
c_in : (insert (~φ') (L.erase (~(φ'⋀ψ'))), R) = c ∨ (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R) = c
⊢ α ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1