>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/CAAfCLngtMa3L6H1%2BpDJVrR0Tdftr%2Brjst82ernqx2_TYBB8kFQ%40mail.gmail.com.
