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