simp [vset.Variational]
α F : Type
s₁ s₂ : vset F α
ρ : SPL.Config F
⊢ {a | (a, ρ) ∈ s₁ ∨ (a, ρ) ∈ s₂} = {a | a ∈ s₁ ∨ a ∈ s₂} | ρ
α F : Type
s₁ s₂ : vset F α
ρ : SPL.Config F
⊢ {a | (a, ρ) ∈ s₁ ∨ (a, ρ) ∈ s₂} = vset.index {a | a ∈ s₁ ∨ a ∈ s₂} ρ