aesop
case ncon
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
L_cond_in : ∅ ⊆ L
precond_eq : {⊥} = {α}
φ✝ ψ✝ : Formula
R_cond_in : {~(φ✝⋀ψ✝)} ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedR (OneSidedLocalRule.ncon φ✝ ψ✝)) (L, R)
⊢ α ∈ c.2 ∨ ∃ res ∈ ∅, res ⊆ c.2
no goals