> Saveliy, could you please comment on that (is it legal to add a disjoint for a and b and what was your intention)?
Yes, it is legal to add or remove disjoints if you need it for the proof. I don't have a very good intuition behind disjoint conditions, so it seems I missed some in the statements. > I used mm-lamp, and it has some automation to prove such steps (no need to write any code, it is available out of the box). ... Will it not break any rules of this initiative, if I show how to prove abaeqb? Sure, please share the video, it would be very interesting to take a look at mm-lamp automation. -- 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/1c4753a2-3855-4a63-9abd-dd79377d248en%40googlegroups.com.
