intros x
case h
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
⊢ ∀ (x : GSNEl × Annotation),
    (((∃ 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)
        x
case h
g : GSN'
recheck revise : vset F GSNEl
ρ : Config F
x : GSNEl × Annotation
⊢ (((∃ 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)
      x