simp [createAnnotation', Set.image]
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ (createAnnotation' g recheck revise | ρ) = createAnnotation (g | ρ) (recheck | ρ) (revise | ρ)
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ (({x | ∃ a b, (a, b) ∈ recheck ∧ ((a, Annotation.Recheck), b) = x} ∪
          {x | ∃ a b, (a, b) ∈ revise ∧ ((a, Annotation.Revise), b) = x} ∪
        {x | ∃ a b, ((a, b) ∈ g ∧ ¬((a, b) ∈ recheck ∨ (a, b) ∈ revise)) ∧ ((a, Annotation.Reuse), b) = x}) |
      ρ) =
    createAnnotation (g | ρ) (recheck | ρ) (revise | ρ)