. apply ih _ _ h
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'
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'