cases' h_stmt with h h <;> rw [h] <;> simp [extendLenOne]
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)
no goals