aesop
case h
α : Formula
R L precond : Finset Formula
ress : List (Finset Formula)
α_in_R : α ∈ R
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.2
no goals