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