{α : Type u} →
  {β : Type v} →
    {P : Sort u_1} →
      {keys : Subarray α} →
        {vals : Subarray β} →
          {a : Std.Slice.size keys = Std.Slice.size vals} →
            {a_1 : Lean.PersistentHashMap.Zipper α β} →
              {keys' : Subarray α} →
                {vals' : Subarray β} →
                  {a' : Std.Slice.size keys' = Std.Slice.size vals'} →
                    {a'_1 : Lean.PersistentHashMap.Zipper α β} →
                      Lean.PersistentHashMap.Zipper.consCollision keys vals a a_1 =
                          Lean.PersistentHashMap.Zipper.consCollision keys' vals' a' a'_1 →
                        (keys ≍ keys' → vals ≍ vals' → a_1 ≍ a'_1 → P) → P