apply Or.inr
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) ≤ 0 ∨ ∃ x ∈ ofLen (len p), toFunction p (len p) ≤ toFunction x (len p)
case h.h
p : LoopProgram
h : toFunction p = diagonal
⊢ ∃ x ∈ ofLen (len p), toFunction p (len p) ≤ toFunction x (len p)