unfold diagonal
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) < diagonal (len p)
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) < Finset.fold max 0 (fun p_1 => toFunction p_1 (len p)) (ofLen (len p)) + 1