Thanks! I have replied in github, hopefully we can figure out what
to do about the issues raised there.
Not too late if anyone else wants to take a look or ask any
questions. I'm always game for talking about iset.mm
and even though
there might still be things to do with the recursion theorem and/or
"seq", I'm pretty excited about making progress on some longstanding
As for the two pull requests, there is now just a combined one at
https://github.com/metamath/set.mm/pull/2588 so hopefully that
removes any confusion about that.