While doing some work, I proved the lemma I needed https://us.metamath.org/mpeuni/bj-elbr.html It turns out it already existed as https://us.metamath.org/mpeuni/brrelex12.html
But when I try to minimize ~bj-elbr, the command `MM-PA> MINIMIZE_WITH *` does not find the 1-step proof from ~brrelex12. Is this a bug ? If I do `MM-PA> DELETE ALL` and then `MM-PA> IMPROVE ALL` it does find the 1-step proof. Thanks, 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/d4bc3088-d3a5-4ff4-963d-c6b46dcc955fn%40googlegroups.com.
