cases orule
α : Formula
R L precond : Finset Formula
ress✝ : List (Finset Formula)
α_in_R : α ∈ R
orule : OneSidedLocalRule precond ress✝
precond_eq : precond = {α}
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)
⊢ α ∈ c.2 ∨ ∃ res ∈ ress✝, res ⊆ c.2
case bot
α : 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)
precond_eq : {⊥} = {α}
⊢ α ∈ c.2 ∨ ∃ res ∈ ∅, res ⊆ c.2

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