simp [←trace_correct]
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        (trace (R | ρ) (sliceSys' S (D.delete ∪ D.modify) | ρ) ∪
            trace (restrict' R D | ρ) (sliceSys' S' (D.add ∪ D.modify) | ρ) ∪
          sliceGSN_V (A | ρ) (trace (R | ρ) (D.delete | ρ))))
      (trace (R | ρ) (D.delete | ρ))
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        (((trace' R (sliceSys' S (D.delete ∪ D.modify)) | ρ) ∪
            trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) | ρ) ∪
          sliceGSN_V (A | ρ) (trace' R D.delete | ρ)))
      (trace' R D.delete | ρ)