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