-- Aesop.Tree.Data
Aesop.GoalData.mk.injEq : ∀ {Rapp MVarCluster : Type} (id : Aesop.GoalId) (parent : IO.Ref MVarCluster) (children : Array (IO.Ref Rapp))
  (origin : Aesop.GoalOrigin) (depth : ℕ) (state : Aesop.GoalState) (isIrrelevant isForcedUnprovable : Bool)
  (preNormGoal : Lean.MVarId) (normalizationState : Aesop.NormalizationState)
  (mvars : Aesop.UnorderedArraySet Lean.MVarId) (forwardState : Aesop.ForwardState)
  (forwardRuleMatches : Aesop.ForwardRuleMatches) (successProbability : Aesop.Percent)
  (addedInIteration lastExpandedInIteration : Aesop.Iteration) (unsafeRulesSelected : Bool)
  (unsafeQueue : Aesop.UnsafeQueue) (failedRapps : Array Aesop.RegularRule) (id_1 : Aesop.GoalId)
  (parent_1 : IO.Ref MVarCluster) (children_1 : Array (IO.Ref Rapp)) (origin_1 : Aesop.GoalOrigin) (depth_1 : ℕ)
  (state_1 : Aesop.GoalState) (isIrrelevant_1 isForcedUnprovable_1 : Bool) (preNormGoal_1 : Lean.MVarId)
  (normalizationState_1 : Aesop.NormalizationState) (mvars_1 : Aesop.UnorderedArraySet Lean.MVarId)
  (forwardState_1 : Aesop.ForwardState) (forwardRuleMatches_1 : Aesop.ForwardRuleMatches)
  (successProbability_1 : Aesop.Percent) (addedInIteration_1 lastExpandedInIteration_1 : Aesop.Iteration)
  (unsafeRulesSelected_1 : Bool) (unsafeQueue_1 : Aesop.UnsafeQueue) (failedRapps_1 : Array Aesop.RegularRule),
  ({ id := id, parent := parent, children := children, origin := origin, depth := depth, state := state,
        isIrrelevant := isIrrelevant, isForcedUnprovable := isForcedUnprovable, preNormGoal := preNormGoal,
        normalizationState := normalizationState, mvars := mvars, forwardState := forwardState,
        forwardRuleMatches := forwardRuleMatches, successProbability := successProbability,
        addedInIteration := addedInIteration, lastExpandedInIteration := lastExpandedInIteration,
        unsafeRulesSelected := unsafeRulesSelected, unsafeQueue := unsafeQueue, failedRapps := failedRapps } =
      { id := id_1, parent := parent_1, children := children_1, origin := origin_1, depth := depth_1, state := state_1,
        isIrrelevant := isIrrelevant_1, isForcedUnprovable := isForcedUnprovable_1, preNormGoal := preNormGoal_1,
        normalizationState := normalizationState_1, mvars := mvars_1, forwardState := forwardState_1,
        forwardRuleMatches := forwardRuleMatches_1, successProbability := successProbability_1,
        addedInIteration := addedInIteration_1, lastExpandedInIteration := lastExpandedInIteration_1,
        unsafeRulesSelected := unsafeRulesSelected_1, unsafeQueue := unsafeQueue_1, failedRapps := failedRapps_1 }) =
    (id = id_1 ∧
      parent = parent_1 ∧
        children = children_1 ∧
          origin = origin_1 ∧
            depth = depth_1 ∧
              state = state_1 ∧
                isIrrelevant = isIrrelevant_1 ∧
                  isForcedUnprovable = isForcedUnprovable_1 ∧
                    preNormGoal = preNormGoal_1 ∧
                      normalizationState = normalizationState_1 ∧
                        mvars = mvars_1 ∧
                          forwardState = forwardState_1 ∧
                            forwardRuleMatches = forwardRuleMatches_1 ∧
                              successProbability = successProbability_1 ∧
                                addedInIteration = addedInIteration_1 ∧
                                  lastExpandedInIteration = lastExpandedInIteration_1 ∧
                                    unsafeRulesSelected = unsafeRulesSelected_1 ∧
                                      unsafeQueue = unsafeQueue_1 ∧ failedRapps = failedRapps_1)