rename_i L R ress O B_def
case mk
B : List TNode
L✝ R✝ : List Formula
ress✝ : List TNode
O✝ : Option (NegLoadFormula ⊕ NegLoadFormula)
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress✝
preconP : Lcond.Sublist L✝ ∧ Rcond.Sublist R✝ ∧ Ocond ⊆ O✝
hC✝ : B = applyLocalRule rule (L✝, R✝, O✝)
⊢ ∀ Y ∈ B, lt_TNode Y (L✝, R✝, O✝)
case mk
B : List TNode
L R : List Formula
ress : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ Ocond ⊆ O
B_def : B = applyLocalRule rule (L, R, O)
⊢ ∀ Y ∈ B, lt_TNode Y (L, R, O)