RESQ_GEN_TAC

res_quanLib.RESQ_GEN_TAC : tactic

Strips the outermost restricted universal quantifier from the conclusion of a goal.

When applied to a goal A ?- !x::P. t, the tactic RESQ_GEN_TAC reduces it to a new goal A,P x' ?- t[x'/x] where x' is a variant of x chosen to avoid clashing with any variables free in the goal’s assumption list. Normally x' is just x.

     A ?- !x::P. t
   ===================  RESQ_GEN_TAC
    A,P x' ?- t[x'/x]

Failure

Fails unless the goal’s conclusion is a restricted universal quantification.

The tactic REPEAT RESQ_GEN_TAC strips away a series of restricted universal quantifiers, and is commonly used before tactics relying on the underlying term structure.

See also

res_quanLib.RESQ_SPEC, res_quanLib.RESQ_SPECL, Tactic.STRIP_TAC, Tactic.GEN_TAC, Tactic.X_GEN_TAC