> On May 14, 2021, at 8:17 AM, Norman Megill <[email protected]> wrote:
>
> I think that removing dependence on AC is usually a good thing.
I agree.
If the proof is much more complex without AC, I think it can be a good idea to
keep the original “simpler” proof as ALT proof. In that case, I strongly
recommend noting *WHY* this is being kept, in this case, because using AC makes
it “much simpler” to prove.
--- David A. Wheeler
--
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/30CE5A42-5E81-4A1E-B22C-1AC78F3E1649%40dwheeler.com.
