apply funext
ρ : 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)
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))