rw [Nat.succ_add, Nat.succ_add, Nat.succ_eq_add_one]
case succ.refine'_1
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := x' } { index := y } n ∈ ofLen (Nat.succ x' + y + n)

case succ.refine'_2
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈ extendLenOne (stmt { index := x' } { index := y } n)
case succ.refine'_1
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := x' } { index := y } n ∈ ofLen (x' + y + n + 1)

case succ.refine'_2
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈ extendLenOne (stmt { index := x' } { index := y } n)