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