simp [trace, setOf]
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ (fun x => ((fun x => (x.1.2, x.2)) '' {e | e ∈ t ∧ (e.1.1, e.2) ∈ es}) (x, ρ)) =
    trace (fun x => t (x, ρ)) fun x => es (x, ρ)
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ (fun x => ((fun x => (x.1.2, x.2)) '' fun e => e ∈ t ∧ (e.1.1, e.2) ∈ es) (x, ρ)) =
    (fun x => x.2) '' fun e => (e ∈ fun x => t (x, ρ)) ∧ e.1 ∈ fun x => es (x, ρ)