\doc{Accessible quantifiers}
\ref{accessible}

The \cflink{fix} and \cflink{instantiate} commands, together with the
\dlink{../proof/by-generalization}{generalization} and
\dlink{../proof/by-specialization}{specialization} proof methods, enable users
to eliminate quantifiers from facts and conjectures.  For a quantifier to be
eliminable, it must be \def{accessible}, that is, it must not be in the scope
of another (explicit or implicit) quantifier over the same variable.