cases orule'
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
Rcond' : Finset Formula
R_cond_in : Rcond' ⊆ R
ress : List (Finset Formula)
orule' : OneSidedLocalRule Rcond' ress
φ ψ : Formula
c_in : ∃ a ∈ ress, (L, R \ Rcond' ∪ a) = c
precond_eq : ~(φ⋀ψ) = α
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2
case bot
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
R_cond_in : {⊥} ⊆ R
c_in : ∃ a ∈ ∅, (L, R \ {⊥} ∪ a) = c
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2

case not
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ✝ : Formula
R_cond_in : {φ✝, ~φ✝} ⊆ R
c_in : ∃ a ∈ ∅, (L, R \ {φ✝, ~φ✝} ∪ a) = c
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2

case neg
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ✝ : Formula
R_cond_in : {~~φ✝} ⊆ R
c_in : ∃ a ∈ [{φ✝}], (L, R \ {~~φ✝} ∪ a) = c
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2

case con
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ✝ ψ✝ : Formula
R_cond_in : {φ✝⋀ψ✝} ⊆ R
c_in : ∃ a ∈ [{φ✝, ψ✝}], (L, R \ {φ✝⋀ψ✝} ∪ a) = c
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2

case ncon
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ✝ ψ✝ : Formula
R_cond_in : {~(φ✝⋀ψ✝)} ⊆ R
c_in : ∃ a ∈ [{~φ✝}, {~ψ✝}], (L, R \ {~(φ✝⋀ψ✝)} ∪ a) = c
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2