∀ {constDecls : Std.HashSet Lean.Syntax.Range}
  {fvarDefs : Std.HashMap Lean.Syntax.Range Lean.Linter.UnusedVariables.FVarDefinition}
  {fvarUses : Std.HashSet Lean.FVarId} {fvarAliases : Std.HashMap Lean.FVarId Lean.FVarId}
  {assignments : Array (Lean.PersistentHashMap Lean.MVarId Lean.Expr)} {constDecls_1 : Std.HashSet Lean.Syntax.Range}
  {fvarDefs_1 : Std.HashMap Lean.Syntax.Range Lean.Linter.UnusedVariables.FVarDefinition}
  {fvarUses_1 : Std.HashSet Lean.FVarId} {fvarAliases_1 : Std.HashMap Lean.FVarId Lean.FVarId}
  {assignments_1 : Array (Lean.PersistentHashMap Lean.MVarId Lean.Expr)},
  { constDecls := constDecls, fvarDefs := fvarDefs, fvarUses := fvarUses, fvarAliases := fvarAliases,
        assignments := assignments } =
      { constDecls := constDecls_1, fvarDefs := fvarDefs_1, fvarUses := fvarUses_1, fvarAliases := fvarAliases_1,
        assignments := assignments_1 } →
    constDecls = constDecls_1 ∧
      fvarDefs = fvarDefs_1 ∧ fvarUses = fvarUses_1 ∧ fvarAliases = fvarAliases_1 ∧ assignments = assignments_1