apply Eq.symm
case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ size n✝ = succ (size n✝) - 1

case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ bit b✝ n✝ ≠ 0
case f.h
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ succ (size n✝) - 1 = size n✝

case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ bit b✝ n✝ ≠ 0