simp [setOf, ←(and_or_left)]
ρ : Config F
t : TraceRel'
d : Delta'
⊢ (fun x =>
      {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} (x, ρ)) =
    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)) =
    restrict (fun x => t (x, ρ)) (indexDelta d ρ)