case succ sz ih =>
  match n with
  | .I m => simp [logic1, logic2, ih]
  | .O m => simp [logic1, logic2, ih]
sz : ℕ
ih : ∀ (n : FinInt sz), logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n minusOne
n : FinInt (Nat.succ sz)
⊢ logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n (I minusOne)
no goals