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