split
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')
case h_1
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
n✝ : FinInt (sz + 0 + 1)
m✝ : FinInt (sz + 0)
heq✝ : addfull n' m' = next false m✝
⊢ toUint (next (dn && dm) (next (dn != dm) m✝)) = toUint (next dn n') + toUint (next dm m')

case h_2
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
n✝ : FinInt (sz + 0 + 1)
m✝ : FinInt (sz + 0)
heq✝ : addfull n' m' = next true m✝
⊢ toUint (next (dn || dm) (next (dn == dm) m✝)) = toUint (next dn n') + toUint (next dm m')