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.con φ' ψ')) (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 φ' (insert ψ' (R.erase (φ'⋀ψ'))))
⊢ (α = φ' ∨ α = ψ' ∨ ¬α = φ'⋀ψ') ∨ {φ, ψ} ⊆ insert φ' (insert ψ' (R.erase (φ'⋀ψ')))