{Rapp MVarCluster : Type} →
  {motive : Aesop.GoalData Rapp MVarCluster → Sort u} →
    (t : Aesop.GoalData Rapp MVarCluster) →
      ((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) →
                                          motive
                                            { 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 }) →
        motive t