case oneSidedR ress orule' =>
  cases orule
  case bot =>
    cases orule'
    all_goals aesop
  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
  case neg φ =>
    cases orule'
    case neg φ' =>
      simp_all
      subst c_in
      subst precond_eq
      if φ = φ'
      then simp_all
      else simp_all
    all_goals aesop
  case con φ ψ =>
    cases orule'
    case con φ' ψ' =>
      simp_all
      subst c_in
      subst precond_eq
      if φ = φ' ∧ ψ = ψ'
      then
        apply Or.inr
        refine Finset.insert_subset_iff.mpr ?_
        aesop
      else aesop
    all_goals aesop
  case ncon φ ψ =>
    simp_all
    cases orule'
    case ncon φ' ψ' =>
      simp at c_in
      subst precond_eq
      cases c_in
      case inl c_eq =>
        subst c_eq
        if φ = φ'
        then simp_all
        else aesop
      case inr c_eq =>
        subst c_eq
        if ψ = ψ'
        then simp_all
        else aesop
    all_goals aesop
α : Formula
R L precond : Finset Formula
ress✝ : List (Finset Formula)
α_in_R : α ∈ R
orule : OneSidedLocalRule precond ress✝
precond_eq : precond = {α}
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)
⊢ α ∈ c.2 ∨ ∃ res ∈ ress✝, res ⊆ c.2
no goals