{α : Type u} →
  {motive_1 : Lean.PersistentArrayNode α → Sort u_1} →
    {motive_2 : Array (Lean.PersistentArrayNode α) → Sort u_1} →
      {motive_3 : List (Lean.PersistentArrayNode α) → Sort u_1} →
        ((cs : Array (Lean.PersistentArrayNode α)) → motive_2 cs → motive_1 (Lean.PersistentArrayNode.node cs)) →
          ((vs : Array α) → motive_1 (Lean.PersistentArrayNode.leaf vs)) →
            ((toList : List (Lean.PersistentArrayNode α)) → motive_3 toList → motive_2 { toList := toList }) →
              motive_3 [] →
                ((head : Lean.PersistentArrayNode α) →
                    (tail : List (Lean.PersistentArrayNode α)) →
                      motive_1 head → motive_3 tail → motive_3 (head :: tail)) →
                  (t : Lean.PersistentArrayNode α) → motive_1 t