Sorry, I misread Mario's post. It looks like we agree on F/2 from an intuitionitic point of view. Then why not take the same definition for set.mm ?
In any case, I will not do this right now and I would first write a draft in my mathbox before making any change. -- 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/f9b254e6-6185-4c1b-81f4-a3026df583a9%40googlegroups.com.
