apply Finset.subset_of_eq at precond_eq
α : 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
R_cond_in : ∅ ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL orule') (L, R)
φ : Formula
precond_eq : {φ, ~φ} = {α}
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1
α : 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
R_cond_in : ∅ ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL orule') (L, R)
φ : Formula
precond_eq : {φ, ~φ} ⊆ {α}
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1