simp_all
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
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)
φ ψ : Formula
precond_eq : {~(φ⋀ψ)} = {α}
⊢ α ∈ c.2 ∨ ∃ res ∈ [{~φ}, {~ψ}], res ⊆ c.2
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
Rcond' : Finset Formula
R_cond_in : Rcond' ⊆ R
ress : List (Finset Formula)
orule' : OneSidedLocalRule Rcond' ress
φ ψ : Formula
c_in : ∃ a ∈ ress, (L, R \ Rcond' ∪ a) = c
precond_eq : ~(φ⋀ψ) = α
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2