case con φ' ψ' =>
  simp_all
  subst c_in
  subst precond_eq
  if φ = φ' ∧ ψ = ψ'
  then
    apply Or.inr
    refine Finset.insert_subset_iff.mpr ?_
    aesop
  else aesop
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
φ' ψ' : Formula
L_cond_in : {φ'⋀ψ'} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.con φ' ψ')) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.1
no goals