apply LoopProgram.len_gt_zero p
case h
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ ?n > ?m

case a
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ ?n ≤ ?m

case n
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ ℕ

case m
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ ℕ
case a
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ len p ≤ 0