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