exists p
case h.h
p : LoopProgram
h : toFunction p = diagonal
⊢ ∃ x ∈ ofLen (len p), toFunction p (len p) ≤ toFunction x (len p)
case h.h
p : LoopProgram
h : toFunction p = diagonal
⊢ p ∈ ofLen (len p) ∧ toFunction p (len p) ≤ toFunction p (len p)