I have an updated version of the video "Introduction to Metamath-lamp, part 2": https://youtu.be/WOp2xQ8mEE4 In this video I've improved the explanation around addition is associative, and also added a demonstration that metamath-lamp's automation could have found it directly.
Last-minute comments welcome. It's currently unlisted; I soon plan to switch it to "public". Part 1 now has the last few useless seconds removed: https://youtu.be/b-RfoUuQpAQ and again, I plan to switch this from "unlisted" to "public" soon. --- 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/A2D5D152-F042-4921-B5C9-AD052F1680F1%40dwheeler.com.
