cases rule <;>
( rename_i rule
  cases rule
  all_goals aesop)
Lcond Rcond : Finset Formula
ress : List SubPair
rule : LocalRule (Lcond, Rcond) ress
res : SubPair
in_ress : res ∈ ress
⊢ Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
no goals