∀ {motive : ℕ → Sort u} {zero : motive 0}
  {bit : (b : Bool) → (n : ℕ) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)} (b : Bool) (n : ℕ)
  (h : n = 0 → b = true), Nat.binaryRec' zero bit (Nat.bit b n) = bit b n h (Nat.binaryRec' zero bit n)