Equations
- countably_infinite.bool_times_nat = {to_fun := λ (bn : bool × ℕ), ite (bn.fst = tt) ((bn.snd) * 2) ((bn.snd) * 2 + 1), inv_fun := λ (d : ℕ), (to_bool (d % 2 = 0) (nat.decidable_eq (d % 2) 0), d / 2), left_inv := countably_infinite.bool_times_nat._proof_1, right_inv := countably_infinite.bool_times_nat._proof_2}
Note: this declaration is incomplete and uses sorry.