{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} → Aesop.GoalUnsafe → Sort (max 1 u)