These are all good questions. 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). I want to record a video with some explanations on how I proved abaeqb. This is a good example for me to demonstrate automation capabilities of mm-lamp. Will it not break any rules of this initiative, if I show how to prove abaeqb?
I’d be really interested in seeing such a video -- 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/24bfcdaa-16ac-4719-a64d-13608d003a71n%40googlegroups.com.
