Theorem: liftedSet.index_mem (Var/liftedSet.lean)

State before:
F α : Type
x : α
ρ : SPL.Config F
s : vset F α
⊢ (x ∈ s | ρ) = ((x, ρ) ∈ s)
Tactic:
simp [vset.Variational, Set.mem_def]
State after:
no goals