Curious how this relates to what lean4 is doing, I guess in lean's case some of the data structures are special cased (Array) and there is no easy way to implement such data structures yourself