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
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
c_in : ∃ a ∈ [{~φ'}, {~ψ'}], (L, R \ {~(φ'⋀ψ')} ∪ a) = c
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2
no goals