apply ofLen_contains_extendLenOne_image
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ loop { index := Nat.zero } p ∈ ofLen (n + 1 + Nat.zero + 1)
case h₁
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ ?p ∈ ofLen (n + 1)

case h₂
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ loop { index := Nat.zero } p ∈ extendLenOne ?p

case p
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ LoopProgram