Challenge completed: https://github.com/GinoGiotto/set.mm/blob/adv2025/adv2025.mm
Note: I believe ~puzzlelem requires ~ax-gl for its proof, even tho there was no "now you can use ~ax-gl again" in the comment. -- 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 visit https://groups.google.com/d/msgid/metamath/5191cfd7-f9a5-4ad2-aa11-da614f91e895n%40googlegroups.com.
