cases orule'
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
Rcond' : Finset Formula
R_cond_in : Rcond' ⊆ R
ress : List (Finset Formula)
L_cond_in : ∅ ⊆ L
orule' : OneSidedLocalRule Rcond' ress
c_in : c ∈ applyLocalRule (LocalRule.oneSidedR orule') (L, R)
φ : Formula
precond_eq : {~~φ} = {α}
⊢ α ∈ c.2 ∨ ∃ res ∈ [{φ}], res ⊆ c.2
case bot
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
L_cond_in : ∅ ⊆ L
φ : Formula
precond_eq : {~~φ} = {α}
R_cond_in : {⊥} ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedR OneSidedLocalRule.bot) (L, R)
⊢ α ∈ c.2 ∨ ∃ res ∈ [{φ}], res ⊆ c.2

case not
α : 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.not φ✝)) (L, R)
⊢ α ∈ c.2 ∨ ∃ res ∈ [{φ}], res ⊆ c.2

case neg
α : 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

case con
α : 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

case ncon
α : 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.ncon φ✝ ψ✝)) (L, R)
⊢ α ∈ c.2 ∨ ∃ res ∈ [{φ}], res ⊆ c.2