{α : Type u_1} →
  {β : Type u_2} →
    (motive : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β) → Sort u_3) →
      (entry : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) →
        (Unit → motive Lean.PersistentHashMap.Entry.null) →
          ((node : Lean.PersistentHashMap.Node α β) → motive (Lean.PersistentHashMap.Entry.ref node)) →
            ((k' : α) → (v' : β) → motive (Lean.PersistentHashMap.Entry.entry k' v')) → motive entry