{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} →
                          (t : Aesop.GoalUnsafe) →
                            ((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)) →
                                                              motive_1 t