apply ofLen_stmt_complete
p : LoopProgram
x y n : ℕ
⊢ add { index := x } { index := y } n ∈ ofLen (len (add { index := x } { index := y } n))
case h_stmt
p : LoopProgram
x y n : ℕ
⊢ add = add ∨ add = sub