match h: p.len with
| 0 => exact False.elim $ Nat.ne_of_gt p.len_gt_zero h
| 1 =>
  dsimp [ofLen, baseProgram]
  apply Finset.mem_union_right
  apply Finset.mem_image_of_mem
  exact lenOne_complete _ h
| n + 1 =>
  apply ofLen_contains_extendLenOne_image
  rw [<- Nat.succ_eq_add_one, <- h]
  apply ofLen_complete
  cases p <;> simp [extendLenOne]
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)
case succ
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := Nat.succ x' } p ∈ ofLen (len p + Nat.succ x' + 1)