{Rapp MVarCluster : Type} →
  {P : Sort u} →
    {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' : 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 := 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', 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' →
                                                                              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' →
                                                                                                                  P) →
                                                                            P