Excellent. So I just happened to stumble upon a nice method used to organize related deductions. Much appreciated.
On Fri, Oct 25, 2019 at 06:24:40AM -0700, Jim Kingdon wrote: > This is relatively common when people want related theorems to have the same > hypothesis. > > If you look at set.mm, you'll see that oveq1i.1 only appears once, but in a > ${ $} block which includes both oveq1i and oveq2i . > > On 10/25/19 2:51 AM, heiphoh...@wilsonb.com 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 metamath+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/eddf8e5b-8733-4ebd-26fd-598253221bb3%40panix.com. -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/20191026034250.GB15709%40lang.