refine' ⟨stmt (.mk 0) (.mk 0) n', ⟨ofLen_stmt_complete _ h_stmt, _⟩⟩
case zero.zero.succ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
n' : ℕ
⊢ ∃ x ∈ ofLen (Nat.zero + Nat.zero + Nat.succ n'),
    stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈ extendLenOne x
case zero.zero.succ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
n' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈ extendLenOne (stmt { index := 0 } { index := 0 } n')