∀ {α : Type u} {β : Type v} {motive_1 : Lean.PersistentHashMap.Node α β → Sort u_1}
  {motive_2 : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → Sort u_1}
  {motive_3 : List (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → Sort u_1}
  {motive_4 : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β) → Sort u_1}
  (t : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)))
  (F_1 : (t : Lean.PersistentHashMap.Node α β) → t.below → motive_1 t)
  (F_2 :
    (t : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
      Lean.PersistentHashMap.Node.below_1 t → motive_2 t)
  (F_3 :
    (t : List (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
      Lean.PersistentHashMap.Node.below_2 t → motive_3 t)
  (F_4 :
    (t : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) →
      Lean.PersistentHashMap.Node.below_3 t → motive_4 t),
  Lean.PersistentHashMap.Node.brecOn_1 t F_1 F_2 F_3 F_4 =
    F_2 t (Lean.PersistentHashMap.Node.brecOn_1.go t F_1 F_2 F_3 F_4).2