module TerminationMixingTupledCurried where

data Nat : Set where
    zero : Nat
    succ : Nat -> Nat

data _×_ (A B : Set) : Set where
    _,_ : A -> B -> A × B

good : Nat × Nat -> Nat -> Nat
good (succ x , y) z = good (x , succ y) (succ z)
good (x , succ y) z = good (x , y) x
good xy (succ z) = good xy z
good _ _ = zero