simp [←Set.setOf_or, Variational.index]
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 | ρ)
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ vset.index
      {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}
      ρ =
    createAnnotation (vset.index g ρ) (vset.index recheck ρ) (vset.index revise ρ)