cases r
case intro
R L : Finset Formula
c : TNode
Rcond' : Finset Formula
R_cond_in : Rcond' ⊆ R
ress : List (Finset Formula)
orule' : OneSidedLocalRule Rcond' ress
φ : Formula
c_in : ∃ a ∈ ress, (L, R \ Rcond' ∪ a) = c
α_in_R : φ ∈ R
r : ~φ = φ
⊢ φ ∈ c.2
no goals