I agree that ax7v does have some form of "binding" for z from x and that ax7 does not. However, because ax7 depends on ax7v, it requires x to be bound regardless of what the outcome is.
I've also read that part of the documentation, like I stated originally, but "Variable Inference" is not a section in the current version of the documentation, and the old documentation has outdated syntax. On Tuesday, May 5, 2026 at 1:31:53 PM UTC-4 [email protected] wrote: > From my vague understanding, I think that none of the variables in > > `theorem ax7{x y z .t: setvar}: $ x =s y -> x =s z -> y =s z $` > are bound to each other. They are all of type "setvar", and this type does > not depend on any variable. So no actual binding is happening, despite all > the variables being a "bound variable". > > Contrast with > > `theorem ax7v{x: setvar} (y: setvar) (z: setvar x): $ x =s y -> x =s z -> > y =s z $ = 'ax_7;` > where z's type depends on x, so x is ..."actively" bound or something > > > Relevant part of the documentation > https://github.com/digama0/mm0/blob/master/mm0.md: A binder enclosed in > curly braces as in `{x: set}` denotes a bound variable, which may appear in > dependencies of other types (see "Variable Inference"). > -- 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 visit https://groups.google.com/d/msgid/metamath/3d25635d-8514-4015-b4b0-c7ea4a99c690n%40googlegroups.com.
