Hi Richard, I've been meaning to move it to Main for a while but haven't found time/motivation to do it yet... I'll try and do it this week. My plan was simply to swap bj-df-if and bj-dfif5, since they are proved equivalent by ~cases2, and leave the rest unchanged. I haven't checked if your method makes the total proof length shorter. I'll make the PR asap so we can discuss on concrete grounds. Benoît
-- 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/b26053a2-ae3b-4878-9ab0-49071d13895d%40googlegroups.com.
