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
φ ψ : Formula
c_in : ∃ a ∈ ress, (L \ Lcond' ∪ a, R) = c
precond_eq : ~(φ⋀ψ) = α
⊢ α ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1
case bot
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
L_cond_in : {⊥} ⊆ L
c_in : ∃ a ∈ ∅, (L \ {⊥} ∪ a, R) = c
⊢ α ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1

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

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

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

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