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)
m : FinInt sz
⊢ logic1 (fun x => !x) (I m) = logic2 (fun x x_1 => x != x_1) (I m) (I minusOne)
no goals