case false
n : ℕ
⊢ bit false n = 2 * n + bif false then 1 else 0

case true
n : ℕ
⊢ bit true n = 2 * n + bif true then 1 else 0
b : Bool
n : ℕ
⊢ bit b n = 2 * n + bif b then 1 else 0
cases b
case true
n : ℕ
⊢ bit true n = 2 * n + bif true then 1 else 0
case false
n : ℕ
⊢ bit false n = 2 * n + bif false then 1 else 0

case true
n : ℕ
⊢ bit true n = 2 * n + bif true then 1 else 0
apply bit0_val
no goals
case true
n : ℕ
⊢ bit true n = 2 * n + bif true then 1 else 0
apply bit1_val