LP, the Larch Prover -- Accessible quantifiers
The fix and instantiate commands, together with the
generalization and
specialization proof methods, enable users
to eliminate quantifiers from facts and conjectures. For a quantifier to be
eliminable, it must be accessible, that is, it must not be in the scope
of another (explicit or implicit) quantifier over the same variable.