∀ (slots : Array Aesop.Slot) (conclusionDeps : Array Aesop.PremiseIndex) (variableMap : Aesop.VariableMap)
  (completeMatches : Lean.PHashSet Aesop.Match) (haveHypForEachSlot : Bool) (slotQueues : Array (Array Aesop.RawHyp))
  (slotQueues_size : slotQueues.size = slots.size) (slots_1 : Array Aesop.Slot)
  (conclusionDeps_1 : Array Aesop.PremiseIndex) (variableMap_1 : Aesop.VariableMap)
  (completeMatches_1 : Lean.PHashSet Aesop.Match) (haveHypForEachSlot_1 : Bool)
  (slotQueues_1 : Array (Array Aesop.RawHyp)) (slotQueues_size_1 : slotQueues_1.size = slots_1.size),
  ({ slots := slots, conclusionDeps := conclusionDeps, variableMap := variableMap, completeMatches := completeMatches,
        haveHypForEachSlot := haveHypForEachSlot, slotQueues := slotQueues, slotQueues_size := slotQueues_size } =
      { slots := slots_1, conclusionDeps := conclusionDeps_1, variableMap := variableMap_1,
        completeMatches := completeMatches_1, haveHypForEachSlot := haveHypForEachSlot_1, slotQueues := slotQueues_1,
        slotQueues_size := slotQueues_size_1 }) =
    (slots = slots_1 ∧
      conclusionDeps = conclusionDeps_1 ∧
        variableMap = variableMap_1 ∧
          completeMatches = completeMatches_1 ∧ haveHypForEachSlot = haveHypForEachSlot_1 ∧ slotQueues = slotQueues_1)