∀ (normRules : Aesop.Index Aesop.NormRuleInfo) (unsafeRules : Aesop.Index Aesop.UnsafeRuleInfo)
  (safeRules : Aesop.Index Aesop.SafeRuleInfo) (unfoldRules : Lean.PHashMap Lean.Name (Option Lean.Name))
  (forwardRules : Aesop.ForwardIndex) (forwardRuleNames : Lean.PHashSet Aesop.RuleName)
  (rulePatterns : Aesop.RulePatternIndex) (erased : Lean.PHashSet Aesop.RuleName)
  (ruleNames : Lean.PHashMap Lean.Name (Aesop.UnorderedArraySet Aesop.RuleName))
  (normRules_1 : Aesop.Index Aesop.NormRuleInfo) (unsafeRules_1 : Aesop.Index Aesop.UnsafeRuleInfo)
  (safeRules_1 : Aesop.Index Aesop.SafeRuleInfo) (unfoldRules_1 : Lean.PHashMap Lean.Name (Option Lean.Name))
  (forwardRules_1 : Aesop.ForwardIndex) (forwardRuleNames_1 : Lean.PHashSet Aesop.RuleName)
  (rulePatterns_1 : Aesop.RulePatternIndex) (erased_1 : Lean.PHashSet Aesop.RuleName)
  (ruleNames_1 : Lean.PHashMap Lean.Name (Aesop.UnorderedArraySet Aesop.RuleName)),
  ({ normRules := normRules, unsafeRules := unsafeRules, safeRules := safeRules, unfoldRules := unfoldRules,
        forwardRules := forwardRules, forwardRuleNames := forwardRuleNames, rulePatterns := rulePatterns,
        erased := erased, ruleNames := ruleNames } =
      { normRules := normRules_1, unsafeRules := unsafeRules_1, safeRules := safeRules_1, unfoldRules := unfoldRules_1,
        forwardRules := forwardRules_1, forwardRuleNames := forwardRuleNames_1, rulePatterns := rulePatterns_1,
        erased := erased_1, ruleNames := ruleNames_1 }) =
    (normRules = normRules_1 ∧
      unsafeRules = unsafeRules_1 ∧
        safeRules = safeRules_1 ∧
          unfoldRules = unfoldRules_1 ∧
            forwardRules = forwardRules_1 ∧
              forwardRuleNames = forwardRuleNames_1 ∧
                rulePatterns = rulePatterns_1 ∧ erased = erased_1 ∧ ruleNames = ruleNames_1)