cases' x with x'
p✝ : LoopProgram
x : ℕ
p : LoopProgram
⊢ loop { index := x } p ∈ ofLen (len p + x + 1)
case zero
p✝ p : LoopProgram
⊢ loop { index := Nat.zero } p ∈ ofLen (len p + Nat.zero + 1)

case succ
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := Nat.succ x' } p ∈ ofLen (len p + Nat.succ x' + 1)