{motive_1 : Aesop.GoalUnsafe → Sort u} →
  {motive_2 : Aesop.MVarClusterUnsafe → Sort u} →
    {motive_3 : Aesop.RappUnsafe → Sort u} →
      {motive_4 : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe → Sort u} →
        {motive_5 : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe → Sort u} →
          {motive_6 : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe → Sort u} →
            {motive_7 : Array (IO.Ref Aesop.RappUnsafe) → Sort u} →
              {motive_8 : Option (IO.Ref Aesop.RappUnsafe) → Sort u} →
                {motive_9 : Array (IO.Ref Aesop.GoalUnsafe) → Sort u} →
                  {motive_10 : Array (IO.Ref Aesop.MVarClusterUnsafe) → Sort u} →
                    {motive_11 : List (IO.Ref Aesop.RappUnsafe) → Sort u} →
                      {motive_12 : List (IO.Ref Aesop.GoalUnsafe) → Sort u} →
                        {motive_13 : List (IO.Ref Aesop.MVarClusterUnsafe) → Sort u} →
                          ((d : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe) →
                              motive_4 d → motive_1 (Aesop.GoalUnsafe.mk d)) →
                            ((d : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe) →
                                motive_5 d → motive_2 (Aesop.MVarClusterUnsafe.mk d)) →
                              ((d : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe) →
                                  motive_6 d → motive_3 (Aesop.RappUnsafe.mk d)) →
                                ((id : Aesop.GoalId) →
                                    (parent : IO.Ref Aesop.MVarClusterUnsafe) →
                                      (children : Array (IO.Ref Aesop.RappUnsafe)) →
                                        (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_7 children →
                                                                      motive_4
                                                                        { 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 }) →
                                  ((parent? : Option (IO.Ref Aesop.RappUnsafe)) →
                                      (goals : Array (IO.Ref Aesop.GoalUnsafe)) →
                                        (isIrrelevant : Bool) →
                                          (state : Aesop.NodeState) →
                                            motive_8 parent? →
                                              motive_9 goals →
                                                motive_5
                                                  { parent? := parent?, goals := goals, isIrrelevant := isIrrelevant,
                                                    state := state }) →
                                    ((id : Aesop.RappId) →
                                        (parent : IO.Ref Aesop.GoalUnsafe) →
                                          (children : Array (IO.Ref Aesop.MVarClusterUnsafe)) →
                                            (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_10 children →
                                                              motive_6
                                                                { id := id, parent := parent, children := children,
                                                                  state := state, isIrrelevant := isIrrelevant,
                                                                  appliedRule := appliedRule,
                                                                  scriptSteps? := scriptSteps?,
                                                                  originalSubgoals := originalSubgoals,
                                                                  successProbability := successProbability,
                                                                  metaState := metaState,
                                                                  introducedMVars := introducedMVars,
                                                                  assignedMVars := assignedMVars }) →
                                      ((toList : List (IO.Ref Aesop.RappUnsafe)) →
                                          motive_11 toList → motive_7 { toList := toList }) →
                                        motive_8 none →
                                          ((val : IO.Ref Aesop.RappUnsafe) → motive_8 (some val)) →
                                            ((toList : List (IO.Ref Aesop.GoalUnsafe)) →
                                                motive_12 toList → motive_9 { toList := toList }) →
                                              ((toList : List (IO.Ref Aesop.MVarClusterUnsafe)) →
                                                  motive_13 toList → motive_10 { toList := toList }) →
                                                motive_11 [] →
                                                  ((head : IO.Ref Aesop.RappUnsafe) →
                                                      (tail : List (IO.Ref Aesop.RappUnsafe)) →
                                                        motive_11 tail → motive_11 (head :: tail)) →
                                                    motive_12 [] →
                                                      ((head : IO.Ref Aesop.GoalUnsafe) →
                                                          (tail : List (IO.Ref Aesop.GoalUnsafe)) →
                                                            motive_12 tail → motive_12 (head :: tail)) →
                                                        motive_13 [] →
                                                          ((head : IO.Ref Aesop.MVarClusterUnsafe) →
                                                              (tail : List (IO.Ref Aesop.MVarClusterUnsafe)) →
                                                                motive_13 tail → motive_13 (head :: tail)) →
                                                            (t : Array (IO.Ref Aesop.GoalUnsafe)) → motive_9 t