intro x y eq
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
⊢ inj f
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
x y : Fin n
eq : f x = f y
⊢ x = y