Hi Freek,
This proposition is hidden from the Mizar author - he cannot quote it, but it is present as a regular proposition in Mizar and in MPTP, so MPTP gives it a name (e3) too. The quotable propositions A3 and A4 are "justified" by this proposition, and they come right after it, so their MPTP names are "e4" and "e5".Aha! So when I am counting the "distance", I'd prefer to _not_ have this "e3" increase the distance. Is there an easy way to somehow take this into account? Is there an easy way to find out which of "your" labels are "quotable" and which ones are not?
Depends on what you consider "easy", but MPTP does not contain this info explicitly now. It is even not present explicitly in the Mizar XML format now. Both can be changed easily, but perhaps the cheapest way for you is then to use the "all-labelling" tools by Robert Milewski. MPTP propositions remember the original Mizar labels, so everything with nonzero original label will then be Mizar-quotable proposition. Once you work with Robert's tools, it might however be easier to switch to using the Mizar implementation completely, there are routines which give you e.g. the proposition kinds for free, etc.
Best, Josef