unfold vset.index
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 ρ)
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, ρ)