∀ (motive : ℕ → ℕ → Sort u_1) (n k : ℕ) (h_1 : Unit → motive 0 0) (h_2 : (n : ℕ) → motive 0 n.succ)
  (h_3 : (n : ℕ) → motive n.succ 0) (h_4 : (n k : ℕ) → motive n.succ k.succ),
  (match n.succ, k.succ with
    | 0, 0 => h_1 ()
    | 0, n.succ => h_2 n
    | n.succ, 0 => h_3 n
    | n.succ, k.succ => h_4 n k) =
    h_4 n k