simp [Set.mem_def]
case h
ρ : Config F
t : TraceRel'
d : Delta'
x : SysEl × GSNEl
⊢ ((x, ρ) ∈ t ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify)) =
    ((x ∈ fun x => t (x, ρ)) ∧ (((x.1, ρ) ∈ d.add ∨ (x.1, ρ) ∈ d.delete) ∨ (x.1, ρ) ∈ d.modify))
no goals