Our hopes and prayers go out to B. Wilson, that he may one day escape his time loop.
(I think it was a moderation error leading to the email getting resent.) Mario On Sat, Oct 26, 2019 at 4:49 AM heiphohmia via Metamath < [email protected]> wrote: > Hello, > > The logical hypothesis for theorem oveq2i has the same name as that for > oveq1i. This tripped me up, but is the naming intentional? > > In particular, I was writing up my own proof of 2p2e4 when I noticed the > clash. In fact, the proof of 2p2e4 exhibits the same exact issue: the first > unification is oveq1i.1=df-2, which is followed by it's parent > eqtr4i.1=oveq2i. Given that 2p2e4 is used as an pedagogical example in MPE, > I feel like I must just be missing something obvious. > > Just in case, I also confirmed the above against HEAD on the develop > branch (commit 2ebe15d3 at the time). > > Forgive the spam if I am just overlooking something > > Cheers, > B. Wilson > > -- > 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/20191026084856.GF24895%40lang. > -- 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/CAFXXJSt6-MqitCmYd6%2Bidb4GAgJmBOAXn%2BE8_L_qjWxn8H5xJQ%40mail.gmail.com.
