case not φ =>
  apply Finset.subset_of_eq at precond_eq
  rw [Finset.subset_singleton_iff'] at precond_eq
  simp_all
  rcases precond_eq with ⟨l,r⟩
  subst l
  cases r
α : 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
no goals