> > Yes, ~hashssle is a specialization of ~hashss and could be replaced (and > removed afterwards). ~hashssle (and ~bj-abf), however, are in mathboxes. In > my opinion, the owners of the mathboxes should be responsible for cleaning > up such cases. But it would be great if a list of such cases was created > and provided after the global minimize action (to be used by the mathbox > owners). >
Regarding: ~bj-abf: it is the same statement as ~abf but it is proved from ~bj-abfal, which is the corresponding closed form. In my opinion, ~bj-abfal should be moved to main (as ~abfal or ~abft ?) and ~abf shoud be proved from it. 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/d04e5157-fd1a-45f3-94dc-5bbbf06e0984%40googlegroups.com.
