cases orule'
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
Lcond' : Finset Formula
L_cond_in : Lcond' ⊆ L
ress : List (Finset Formula)
orule' : OneSidedLocalRule Lcond' ress
R_cond_in : ∅ ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL orule') (L, R)
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.1
case bot
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
L_cond_in : {⊥} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL OneSidedLocalRule.bot) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.1

case not
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
φ✝ : Formula
L_cond_in : {φ✝, ~φ✝} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.not φ✝)) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.1

case neg
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
φ✝ : Formula
L_cond_in : {~~φ✝} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.neg φ✝)) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.1

case con
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
φ✝ ψ✝ : Formula
L_cond_in : {φ✝⋀ψ✝} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.con φ✝ ψ✝)) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.1

case ncon
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
φ✝ ψ✝ : Formula
L_cond_in : {~(φ✝⋀ψ✝)} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.ncon φ✝ ψ✝)) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.1