cases lr'
case mk.intro
α : Formula
L R precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
ress' : List SubPair
Lcond' Rcond' : Finset Formula
lr' : LocalRule (Lcond', Rcond') ress'
L_cond_in : Lcond' ⊆ L
R_cond_in : Rcond' ⊆ R
c_in : c ∈ applyLocalRule lr' (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1
case mk.intro.oneSidedL
α : Formula
L R precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
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)
⊢ α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1

case mk.intro.oneSidedR
α : Formula
L R precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
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.1 ∨ ∃ res ∈ ress, res ⊆ c.1

case mk.intro.LRnegL
α : Formula
L R precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
ϕ✝ : Formula
L_cond_in : {ϕ✝} ⊆ L
R_cond_in : {~ϕ✝} ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.LRnegL ϕ✝) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1

case mk.intro.LRnegR
α : Formula
L R precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
ϕ✝ : Formula
L_cond_in : {~ϕ✝} ⊆ L
R_cond_in : {ϕ✝} ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.LRnegR ϕ✝) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1