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.
