case equal i j =>
  by_cases hv : v i = v j <;> simp[hv, Nat.isEqNat, eq_comm]
k : ℕ
c : Code k
f : Vector ℕ k →. ℕ
n✝ : ℕ
i j : Fin n✝
y : ℕ
v : Fin n✝ → ℕ
⊢ v i = v j ∧ y = 1 ∨ ¬v i = v j ∧ y = 0 ↔ (v i).isEqNat (v j) = y
no goals