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.