cases b with
| true => simpa [← Nat.two_mul] using o _
| false =>
  match n with
  | 0 => exact absurd (hb rfl) Bool.noConfusion
  | n+1 => simpa [← Nat.add_assoc, Nat.add_right_comm _ 1, ← Nat.two_mul] using e _
case f
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
b : Bool
n : ℕ
hb : n = 0 → b = true
a✝ : bit b n = n → C (bit b n)
⊢ C (bit b n)
no goals