plus : {l : Level} {t : Set l} → (x y : ℕ) → (next : ℕ -> t) -> t
plus x zero next = next x
plus x (suc y) next = plus (suc x) y next

-- plus 10 20
--   λ next → next 30