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
α : 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