[STATEMENT]
lemma next_upto_generator [simp]:
  "list.next upto_generator n = (n, n + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.next local.upto_generator n = (n, n + 1)
[PROOF STEP]
by transfer simp