simp [addfull]
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
⊢ toUint (addfull (next dn n') (next dm m')) = toUint (next dn n') + toUint (next dm m')
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
⊢ toUint
      (match addfull n' m' with
      | next false r => next (dn && dm) (next (dn != dm) r)
      | next true r => next (dn || dm) (next (dn == dm) r)) =
    toUint (next dn n') + toUint (next dm m')