[mizar] How to call it?

[trybulec@math.uwb.edu.pl]

Fixed variables are called sometimes local constants. Ground term is 
defined as
'a term that does not contain any variables at all' (Wikipedia).

How to call a term that does not contain bound variables, but local constants
are allowed?

The same goes for closed terms and so on.

BTW How to call variables that are not fixed. I tried to use 
'quantified variables'. It is O.K. in the case of variables bound by 
quatifiers, not so
is they are bound by operators.

So I use 'bound variables'. On the other hand fixed variables are also 
bound, by proof constructors.

Regards,
Andrzej