SPEC_TAC : term * term -> tactic
Generalizes a goal.
When applied to a pair of terms (`u`,`x`), where x is just a variable,
and a goal A ?- t, the tactic SPEC_TAC generalizes the goal to
A ?- !x. t[x/u], that is, all (free) instances of u are turned into x.
A ?- t
================= SPEC_TAC (`u`,`x`)
A ?- !x. t[x/u]
- FAILURE CONDITIONS
Fails unless x is a variable with the same type as u.
Removing unnecessary speciality in a goal, particularly as a prelude to
an inductive proof.
- SEE ALSO
GEN, GENL, GEN_ALL, GEN_TAC, SPEC, SPECL, SPEC_ALL, STRIP_TAC.