rcases precond_eq with ⟨l,r⟩
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
Rcond' : Finset Formula
R_cond_in : Rcond' ⊆ R
ress : List (Finset Formula)
orule' : OneSidedLocalRule Rcond' ress
φ : Formula
c_in : ∃ a ∈ ress, (L, R \ Rcond' ∪ a) = c
precond_eq : φ = α ∧ ~φ = α
⊢ α ∈ c.2
case intro
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
Rcond' : Finset Formula
R_cond_in : Rcond' ⊆ R
ress : List (Finset Formula)
orule' : OneSidedLocalRule Rcond' ress
φ : Formula
c_in : ∃ a ∈ ress, (L, R \ Rcond' ∪ a) = c
l : φ = α
r : ~φ = α
⊢ α ∈ c.2