simpa [← Nat.two_mul] using o _
case f.true
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
n : ℕ
hb : n = 0 → true = true
a✝ : bit true n = n → C (bit true n)
⊢ C (bit true n)
no goals