constructor
case h.h
p : LoopProgram
h : toFunction p = diagonal
⊢ p ∈ ofLen (len p) ∧ toFunction p (len p) ≤ toFunction p (len p)
case h.h.left
p : LoopProgram
h : toFunction p = diagonal
⊢ p ∈ ofLen (len p)

case h.h.right
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) ≤ toFunction p (len p)