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
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
no goals