cases b
sz : ℕ
da : Bool
a' : FinInt sz
ih : ∀ (a b : FinInt (Nat.add sz 0)), toUint a = toUint b → a = b
b : FinInt (Nat.succ (Nat.add sz 0))
h : toUint (next da a') = toUint b
⊢ next da a' = b
case next
sz : ℕ
da : Bool
a' : FinInt sz
ih : ∀ (a b : FinInt (Nat.add sz 0)), toUint a = toUint b → a = b
a✝¹ : Bool
a✝ : FinInt sz
h : toUint (next da a') = toUint (next a✝¹ a✝)
⊢ next da a' = next a✝¹ a✝