feat: Vectors of rFunctors

[Remyjck]

Here is an ongoing attempt to add extensible vectors of rFunctors #37

[markusdemedeiros]

Great start on this :)

One thing I'm thinking about: I'm replacing GenMapOF in my heaps PR to support heaps with infinitely many allocated elements. I'm doing this for other reasons, but because the iProp construction is based on GenMapOF, I'm wondering how much the rest of the inG machinery depends on the number of pieces of ghost state being finite?

[Remyjck]

I think/hope that as long as you carry around a witness that your index is valid (what is being done by GId here), then it should be fine to have infinite pieces of ghost state.

FYI, I do not plan on working on this for the next few weeks, but if/when I do, I would like to swap out Array in the definition of GFunctors with the generalization of gmap from #63

[markusdemedeiros]

Good to know! FYI, before you start working on it again, you should discuss with Mario about if we should stick to the Array definition or the Heaps definition. I think the Heaps definition is super interesting, but we don't want to make the rest of the port too much harder on ourselves.

[markusdemedeiros]

@Remyjck Is it alright with you if adopt this feature? I am starting to work on it in #92.

[Remyjck]

Sorry, I didn't see this until now!
Please go ahead, I haven't given this much thought for a while.

I'm curious to see how this is resolved, I spent quite some time struggling to get the right camera instances bundled in the right places.