simp [←Set.setOf_or, Variational.index]
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (({x | x ∈ t ∧ (x.1.1, x.2) ∈ d.add} ∪ {x | x ∈ t ∧ (x.1.1, x.2) ∈ d.delete} ∪
        {x | x ∈ t ∧ (x.1.1, x.2) ∈ d.modify}) |
      ρ) =
    restrict (t | ρ) (d | ρ)
ρ : Config F
t : TraceRel'
d : Delta'
⊢ vset.index {a | (a ∈ t ∧ (a.1.1, a.2) ∈ d.add ∨ a ∈ t ∧ (a.1.1, a.2) ∈ d.delete) ∨ a ∈ t ∧ (a.1.1, a.2) ∈ d.modify}
      ρ =
    restrict (vset.index t ρ) (indexDelta d ρ)