. show p.toFunction p.len < diagonal p.len
  unfold diagonal
  rw [Nat.lt_add_one_iff, Finset.le_fold_max]
  apply Or.inr
  exists p; constructor
  apply ofLen_complete
  rfl
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ ?a < ?b

case a
p : LoopProgram
h : toFunction p = diagonal
⊢ ?a = ?b

case a
p : LoopProgram
h : toFunction p = diagonal
⊢ ℕ

case b
p : LoopProgram
h : toFunction p = diagonal
⊢ ℕ
case a
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) = diagonal (len p)