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/20191025095154.GA26042%40lang.
