Thank you Mario, this reminded me that to find the substitution for an assertion, you have to process its mandatory hypotheses in order. I was disregarding the ordering.
On Wed, Oct 7, 2020 at 5:50 PM David A. Wheeler <[email protected]> wrote: > On Oct 7, 2020, at 5:11 PM, Mario Carneiro <[email protected]> wrote: ... > > > On Oct 7, 2020, at 5:25 PM, David A. Wheeler <[email protected]> > wrote: > This is a nice answer. > > > We do note this in: http://us.metamath.org/mpeuni/mmset.html#proofs under > “legal syntax”. However, it’s probably too abstract as it’s currently > written. I plan to tweak this question & answer as a proposed extension to > the “legal syntax” part, because this specific answer may make it much > clearer. > > > I tried to capture this discussion in this pull request: > https://github.com/metamath/set.mm/pull/1843 > > > -- > 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/EF1ED7AC-55A0-499B-A104-7964FF5843B2%40dwheeler.com > <https://groups.google.com/d/msgid/metamath/EF1ED7AC-55A0-499B-A104-7964FF5843B2%40dwheeler.com?utm_medium=email&utm_source=footer> > . > -- 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/CAE4YSNSN6wD2XG3hv9aBNyRC%3DzsGDo4O0fAJRoHR9zRaOB5P_w%40mail.gmail.com.
