∀ {oldGoal newGoal : Lean.MVarId} {addedFVars removedFVars : Std.HashSet Lean.FVarId} {targetChanged : Bool}
  {oldGoal_1 newGoal_1 : Lean.MVarId} {addedFVars_1 removedFVars_1 : Std.HashSet Lean.FVarId} {targetChanged_1 : Bool},
  { oldGoal := oldGoal, newGoal := newGoal, addedFVars := addedFVars, removedFVars := removedFVars,
        targetChanged := targetChanged } =
      { oldGoal := oldGoal_1, newGoal := newGoal_1, addedFVars := addedFVars_1, removedFVars := removedFVars_1,
        targetChanged := targetChanged_1 } →
    oldGoal = oldGoal_1 ∧
      newGoal = newGoal_1 ∧ addedFVars = addedFVars_1 ∧ removedFVars = removedFVars_1 ∧ targetChanged = targetChanged_1