intro c c_in
α : Formula
R L : Finset Formula
C : List TNode
precond : Finset Formula
ress : List (Finset Formula)
α_in_R : α ∈ R
lrApp : LocalRuleApp (L, R) C
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
⊢ ∀ c ∈ C, α ∈ c.2 ∨ ∃ res ∈ ress, res ⊆ c.2
α : Formula
R L : Finset Formula
C : List TNode
precond : Finset Formula
ress : List (Finset Formula)
α_in_R : α ∈ R
lrApp : LocalRuleApp (L, R) C
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
c_in : c ∈ C
⊢ α ∈ c.2 ∨ ∃ res ∈ ress, res ⊆ c.2