∀ {pos goals selectedLocations replaceRange pos_1 goals_1 selectedLocations_1 replaceRange_1 : Lean.Json},
  { pos := pos, goals := goals, selectedLocations := selectedLocations, replaceRange := replaceRange } =
      { pos := pos_1, goals := goals_1, selectedLocations := selectedLocations_1, replaceRange := replaceRange_1 } →
    pos = pos_1 ∧ goals = goals_1 ∧ selectedLocations = selectedLocations_1 ∧ replaceRange = replaceRange_1