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