cases rule
Lcond Rcond : Finset Formula
ress : List SubPair
rule : LocalRule (Lcond, Rcond) ress
res : SubPair
ress_in_ress : res ∈ ress
ℓ : Char
ℓ_in_res : ℓ ∈ voc res.2
⊢ ℓ ∈ voc Rcond
case oneSidedL
Lcond : Finset Formula
res : SubPair
ℓ : Char
ℓ_in_res : ℓ ∈ voc res.2
ress✝ : List (Finset Formula)
orule✝ : OneSidedLocalRule Lcond ress✝
ress_in_ress : res ∈ List.map (fun res => (res, ∅)) ress✝
⊢ ℓ ∈ voc ∅

case oneSidedR
Rcond : Finset Formula
res : SubPair
ℓ : Char
ℓ_in_res : ℓ ∈ voc res.2
ress✝ : List (Finset Formula)
orule✝ : OneSidedLocalRule Rcond ress✝
ress_in_ress : res ∈ List.map (fun res => (∅, res)) ress✝
⊢ ℓ ∈ voc Rcond

case LRnegL
res : SubPair
ℓ : Char
ℓ_in_res : ℓ ∈ voc res.2
ϕ✝ : Formula
ress_in_ress : res ∈ ∅
⊢ ℓ ∈ voc {~ϕ✝}

case LRnegR
res : SubPair
ℓ : Char
ℓ_in_res : ℓ ∈ voc res.2
ϕ✝ : Formula
ress_in_ress : res ∈ ∅
⊢ ℓ ∈ voc {ϕ✝}