case next db b' =>
cases da <;> cases db <;> simp [toUint] at h <;> simp
. apply ih _ _ h
. have h₁ := @toUint_lt _ a'; have h₂ := @toUint_ge _ b'; sorry_arith
. have h₁ := @toUint_ge _ a'; have h₂ := @toUint_lt _ b'; sorry_arith
. apply ih; sorry_arith
sz : ℕ
da : Bool
a' : FinInt sz
ih : ∀ (a b : FinInt (Nat.add sz 0)), toUint a = toUint b → a = b
db : Bool
b' : FinInt sz
h : toUint (next da a') = toUint (next db b')
⊢ next da a' = next db b'
no goals