rename_i C_eq
case mk.intro
α : Formula
L R : Finset Formula
C : List TNode
precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
c_in : c ∈ C
ress' : List SubPair
Lcond' Rcond' : Finset Formula
lr' : LocalRule (Lcond', Rcond') ress'
hC✝ : C = applyLocalRule lr' (L, R)
L_cond_in : Lcond' ⊆ L
R_cond_in : Rcond' ⊆ R
⊢ α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1
case mk.intro
α : Formula
L R : Finset Formula
C : List TNode
precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
c_in : c ∈ C
ress' : List SubPair
Lcond' Rcond' : Finset Formula
lr' : LocalRule (Lcond', Rcond') ress'
C_eq : C = applyLocalRule lr' (L, R)
L_cond_in : Lcond' ⊆ L
R_cond_in : Rcond' ⊆ R
⊢ α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1