intros S S' A R D ρ
⊢ ∀ (S S' : Sys') (A : GSN') (R : TraceRel') (D : Delta') (ρ : Config F),
    (GSN_IA' S S' A R D | ρ) = GSN_IA (S | ρ) (S' | ρ) (A | ρ) (R | ρ) (D | ρ)
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (GSN_IA' S S' A R D | ρ) = GSN_IA (S | ρ) (S' | ρ) (A | ρ) (R | ρ) (D | ρ)