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, [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/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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/20191026034250.GB15709%40lang.
