Can I get a review on https://github.com/metamath/set.mm/pull/2584 ?
I don't think there is anything especially controversial here (the funinsn part may or may not lead to anything else, but the rest is just the next step in the ongoing work to remove some of the conditions on seq theorems in iset.mm), but I probably shouldn't speculate on whether there are no comments or approvals in github yet.
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8511f9be-25b1-4bc7-2136-4bdca59ee4a8%40panix.com.
