{Goal MVarCluster : Type} →
  {motive : Aesop.RappData Goal MVarCluster → Sort u} →
    ((id : Aesop.RappId) →
        (parent : IO.Ref Goal) →
          (children : Array (IO.Ref MVarCluster)) →
            (state : Aesop.NodeState) →
              (isIrrelevant : Bool) →
                (appliedRule : Aesop.RegularRule) →
                  (scriptSteps? : Option (Array Aesop.Script.LazyStep)) →
                    (originalSubgoals : Array Lean.MVarId) →
                      (successProbability : Aesop.Percent) →
                        (metaState : Lean.Meta.SavedState) →
                          (introducedMVars assignedMVars : Aesop.UnorderedArraySet Lean.MVarId) →
                            motive
                              { id := id, parent := parent, children := children, state := state,
                                isIrrelevant := isIrrelevant, appliedRule := appliedRule, scriptSteps? := scriptSteps?,
                                originalSubgoals := originalSubgoals, successProbability := successProbability,
                                metaState := metaState, introducedMVars := introducedMVars,
                                assignedMVars := assignedMVars }) →
      (t : Aesop.RappData Goal MVarCluster) → motive t