-- Aesop.Tree.Data
Aesop.GoalData.mk.inj : ∀ {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