∀ {pos goals : Lean.Json} {termGoal? : Option Lean.Json} {selectedLocations pos_1 goals_1 : Lean.Json}
  {termGoal?_1 : Option Lean.Json} {selectedLocations_1 : Lean.Json},
  { pos := pos, goals := goals, termGoal? := termGoal?, selectedLocations := selectedLocations } =
      { pos := pos_1, goals := goals_1, termGoal? := termGoal?_1, selectedLocations := selectedLocations_1 } →
    pos = pos_1 ∧ goals = goals_1 ∧ termGoal? = termGoal?_1 ∧ selectedLocations = selectedLocations_1