cases da <;> cases db <;> simp [toUint] at h <;> simp
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'
case false.false
sz : ℕ
a' : FinInt sz
ih : ∀ (a b : FinInt (Nat.add sz 0)), toUint a = toUint b → a = b
b' : FinInt sz
h : toUint a' = toUint b'
⊢ a' = b'

case false.true
sz : ℕ
a' : FinInt sz
ih : ∀ (a b : FinInt (Nat.add sz 0)), toUint a = toUint b → a = b
b' : FinInt sz
h : toUint a' = 2 ^ sz + toUint b'
⊢ False

case true.false
sz : ℕ
a' : FinInt sz
ih : ∀ (a b : FinInt (Nat.add sz 0)), toUint a = toUint b → a = b
b' : FinInt sz
h : 2 ^ sz + toUint a' = toUint b'
⊢ False

case true.true
sz : ℕ
a' : FinInt sz
ih : ∀ (a b : FinInt (Nat.add sz 0)), toUint a = toUint b → a = b
b' : FinInt sz
h : toUint a' = toUint b'
⊢ a' = b'