simp [mem, this]
n : Nat
s : SparseSet n
i : Nat
h : i < s.count
isLt : i < n
this : s[i] = s.dense[i]
⊢ s[i] ∈ s
n : Nat
s : SparseSet n
i : Nat
h : i < s.count
isLt : i < n
this : s[i] = s.dense[i]
⊢ ↑s.sparse[↑s.dense[i]] < s.count ∧ s.dense[↑s.sparse[↑s.dense[i]]] = s.dense[i]