case oneSidedR orule' =>
  apply Or.inl
  aesop
α : Formula
L R precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
Rcond' : Finset Formula
R_cond_in : Rcond' ⊆ R
ress✝ : List (Finset Formula)
L_cond_in : ∅ ⊆ L
orule' : OneSidedLocalRule Rcond' ress✝
c_in : c ∈ applyLocalRule (LocalRule.oneSidedR orule') (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1
no goals