case next sz bn n' =>
cases bn <;> simp [ih]
. sorry_arith
. sorry_arith
sz : ℕ
bn : Bool
n' : FinInt sz
ih : ∀ (n : FinInt (Nat.add sz 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add sz 0 - 1 - toUint n
⊢ toUint (comp (next bn n')) = 2 ^ Nat.succ (Nat.add sz 0) - 1 - toUint (next bn n')
no goals