cases orule <;> aesop
Lcond : Finset Formula
res : SubPair
ℓ : Char
ℓ_in_res : ℓ ∈ voc res.1
ress : List (Finset Formula)
orule : OneSidedLocalRule Lcond ress
ress_in_ress : res ∈ List.map (fun res => (res, ∅)) ress
⊢ ℓ ∈ voc Lcond
no goals