The call REPLICATE n tac gives a new tactic that it equivalent to an n-fold
repetition of tac, i.e. tac THEN tac THEN ... THEN tac.
FAILURE CONDITIONS
The call REPLICATE n tac never fails, but when applied to a goal it will fail
if the tactic does.
EXAMPLE
We might conceivably want to strip off exactly three universal quantifiers from
a goal that contains more than three. We can use REPLICATE_TAC 3 GEN_TAC to
do that.