constructor
⊢ (Function.Injective fun n => next^[n] (0, 0)) ∧ Function.Surjective fun n => next^[n] (0, 0)
case left

⊢ Function.Injective fun n => next^[n] (0, 0)

case right

⊢ Function.Surjective fun n => next^[n] (0, 0)