GEN_TAC : tactic
STRUCTURE
Tactic
SYNOPSIS
Strips the outermost universal quantifier from the conclusion of a goal.
DESCRIPTION
When applied to a goal A ?- !x. t, the tactic GEN_TAC reduces it to A ?- 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. t
   ==============  GEN_TAC
    A ?- t[x'/x]

FAILURE
Fails unless the goal’s conclusion is universally quantified.
USES
The tactic REPEAT GEN_TAC strips away any universal quantifiers, and is commonly used before tactics relying on the underlying term structure.
SEEALSO
FILTER_GEN_TAC, GEN, GENL, GEN_ALL, SPEC, SPECL, SPEC_ALL, SPEC_TAC, STRIP_TAC, X_GEN_TAC
HOL  Kananaskis-13