{α : Type u_1} →
  {β : Type u_3} →
    (motive : Lean.PersistentArrayNode α → β → Sort u_2) →
      (x : Lean.PersistentArrayNode α) →
        (x_1 : β) →
          ((cs : Array (Lean.PersistentArrayNode α)) → (b : β) → motive (Lean.PersistentArrayNode.node cs) b) →
            ((vs : Array α) → (b : β) → motive (Lean.PersistentArrayNode.leaf vs) b) → motive x x_1