simp [restrict, indexDelta, allElements, ←Set.setOf_or, index_mem, setOf]
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (fun x => (x, ρ) ∈ t ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)) =
    restrict (fun x => t (x, ρ)) (indexDelta d ρ)
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (fun x => (x, ρ) ∈ t ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)) = fun x =>
    (x ∈ fun x => t (x, ρ)) ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)