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