simp_all
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
L_cond_in : ∅ ⊆ L
φ : Formula
precond_eq : {~~φ} = {α}
φ' : Formula
R_cond_in : {~~φ'} ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedR (OneSidedLocalRule.neg φ')) (L, R)
⊢ α ∈ c.2 ∨ ∃ res ∈ [{φ}], res ⊆ c.2
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ φ' : Formula
precond_eq : ~~φ = α
R_cond_in : ~~φ' ∈ R
c_in : c = (L, insert φ' (R.erase (~~φ')))
⊢ (α = φ' ∨ ¬α = ~~φ') ∨ φ = φ' ∨ ¬φ = ~~φ' ∧ φ ∈ R