{α : Type u_1} →
  {β : Type u_2} →
    (motive : Lean.PersistentHashMap.CollisionNode α β → ℕ → α → β → Sort u_3) →
      (x : Lean.PersistentHashMap.CollisionNode α β) →
        (x_1 : ℕ) →
          (x_2 : α) →
            (x_3 : β) →
              ((n : Lean.PersistentHashMap.CollisionNode α β) →
                  (keys : Array α) →
                    (vals : Array β) →
                      (heq : keys.size = vals.size) →
                        (property :
                            Lean.PersistentHashMap.IsCollisionNode
                              (Lean.PersistentHashMap.Node.collision keys vals heq)) →
                          (h : n = ⟨Lean.PersistentHashMap.Node.collision keys vals heq, property⟩) →
                            (i : ℕ) →
                              (k : α) →
                                (v : β) →
                                  motive
                                    (namedPattern n ⟨Lean.PersistentHashMap.Node.collision keys vals heq, property⟩ h) i
                                    k v) →
                ((es : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
                    (h : Lean.PersistentHashMap.IsCollisionNode (Lean.PersistentHashMap.Node.entries es)) →
                      (x : ℕ) → (x_4 : α) → (x_5 : β) → motive ⟨Lean.PersistentHashMap.Node.entries es, h⟩ x x_4 x_5) →
                  motive x x_1 x_2 x_3