case inl c_eq =>
  subst c_eq
  if φ = φ'
  then simp_all
  else aesop
R L : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
α_in_R : ~(φ⋀ψ) ∈ R
c_eq : (L, insert (~φ') (R.erase (~(φ'⋀ψ')))) = c
⊢ ~(φ⋀ψ) ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2
no goals