have : p.len + x'.succ = (loop (.mk x') p).len := by rfl
case succ.h₁
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := x' } p ∈ ofLen (len p + Nat.succ x')

case succ.h₂
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := Nat.succ x' } p ∈ extendLenOne (loop { index := x' } p)
case succ.h₁
p✝ p : LoopProgram
x' : ℕ
this : len p + Nat.succ x' = len (loop { index := x' } p)
⊢ loop { index := x' } p ∈ ofLen (len p + Nat.succ x')

case succ.h₂
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := Nat.succ x' } p ∈ extendLenOne (loop { index := x' } p)