all_goals simp_all
case mk.intro.LRnegL
α : Formula
R L precond : Finset Formula
ress : List (Finset Formula)
α_in_R : α ∈ R
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.2 ∨ ∃ res ∈ ress, res ⊆ c.2

case mk.intro.LRnegR
α : Formula
R L precond : Finset Formula
ress : List (Finset Formula)
α_in_R : α ∈ R
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.2 ∨ ∃ res ∈ ress, res ⊆ c.2
no goals