subst c_eq
R L : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
α_in_R : ~(φ⋀ψ) ∈ R
c_eq : (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))) = c
⊢ ~(φ⋀ψ) ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2
R L : Finset Formula
φ ψ φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
α_in_R : ~(φ⋀ψ) ∈ R
⊢ ~(φ⋀ψ) ∈ (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))).2 ∨
    ~φ ∈ (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))).2 ∨ ~ψ ∈ (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))).2