apply ofLen_complete
case h₁
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ ?p ∈ ofLen (len p)

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

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

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
case h₂
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ loop { index := Nat.zero } p ∈ extendLenOne p